Página 1 dos resultados de 8450 itens digitais encontrados em 0.051 segundos

Um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências.; An object-oriented development process with support to inconsistencies formal verification.

Sousa, Thiago Carvalho de
Fonte: Biblioteca Digitais de Teses e Dissertações da USP Publicador: Biblioteca Digitais de Teses e Dissertações da USP
Tipo: Tese de Doutorado Formato: application/pdf
Publicado em 29/11/2013 PT
Relevância na Pesquisa
45.98%
As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto.; The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes...

Measurement of the normalized Z/gamma* -> mu(+)mu(-) transverse momentum distribution in p(p)over-bar collisions at root s=1.96 TeV

Abazov, V. M.; Abbott, B.; Abolins, M.; Acharya, B. S.; Adams, M.; Adams, T.; Aleexev, G. D.; Alkhazov, G.; Alton, A.; Alverson, G.; Alves, G. A.; Ancu, L. S.; Aoki, M.; Arnoud, Y.; Arov, M.; Askew, A.; Asman, B.; Atramentov, O.; Avila, C.; BackusMayes, J
Fonte: Elsevier B.V. Publicador: Elsevier B.V.
Tipo: Artigo de Revista Científica Formato: 522-530
ENG
Relevância na Pesquisa
45.77%
Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq); Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP); We present a new measurement of the Z/gamma* transverse momentum distribution in the range 0-330 GeV, in proton-antiproton collisions at root s = 1.96 TeV. The measurement uses 0.97 fb(-1) of integrated luminosity recorded by the D0 experiment and is the first using the Z/gamma* -> mu(+)mu(-) + X channel at this center-of-mass energy. This is also the first measurement of the Z/gamma* transverse momentum distribution that presents the result at the level of particles entering the detector, minimizing dependence on theoretical models. As any momentum of the Z/gamma* in the plane transverse to the incoming beams must be balanced by some recoiling system, primarily the result of QCD radiation in the initial state, this variable is an excellent probe of the underlying process. Tests of the predictions of QCD calculations and current event generators show they have varied success in describing the data. Using this measurement as an input to theoretical predictions will allow for a better description of hadron collider data and hence it will increase experimental sensitivity to rare signals. (C) 2010 Elsevier B.V. All rights reserved.

Event-by-event fluctuations of transverse momentum and multiparticle clusters in relativistic heavy-ion collisions

Florkowski,W.; Broniowski,W.; Hiller,B.; Bozek,P.
Fonte: Sociedade Brasileira de Física Publicador: Sociedade Brasileira de Física
Tipo: Artigo de Revista Científica Formato: text/html
Publicado em 01/06/2007 EN
Relevância na Pesquisa
45.8%
We analyze the event-by-event fluctuations of mean transverse momentum measured recently by the PHENIX and STAR Collaborations at RHIC. We argue that the observed scaling of strength of dynamical fluctuations with the inverse number of particles can be naturally explained by formation of multiparticle clusters.

Uma biblioteca de padrões de especificação em Event-B para mecanismos de troca de mensagens em sistema distribuídos

Pivetta, Paulo Junior Penna
Fonte: Pontifícia Universidade Católica do Rio Grande do Sul; Porto Alegre Publicador: Pontifícia Universidade Católica do Rio Grande do Sul; Porto Alegre
Tipo: Dissertação de Mestrado
PORTUGUêS
Relevância na Pesquisa
45.91%
O desenvolvimento de sistemas distribuídos e protocolos de comunicação é uma tarefa complexa e o uso de técnicas de especificação e verificação formal torna-se necessário para garantir a corretude de tais sistemas. Enquanto técnicas de model-checking passam pelo problema da explosão do espaço de estados, o uso de provadores de teoremas representa um importante recurso para verificação de sistemas com ilimitado número estados. O método formal Event-B, de uso crescente na indústria e academia, se apóia na técnica de prova de teoremas e suporta refinamento. A contribuição deste trabalho está em proporcionar uma biblioteca reusável de padrões de especificação, em Event-B, de mecanismos de troca de mensagens em sistemas distribuídos. Um padrão de especificação define a semântica de comunicação desejada em um canal, demostrando formalmente suas propriedades. Durante o desenvolvimento de um sistema distribuído, o desenvolvedor pode fazer uso destes padrões através de passos guiados de refinamento do sistema. O sistema resultante garante a semantica de comunicação definida no padrão utilizado e livra o desenvolvedor de se preocupar em definir o sistema de comunicação a partir do início e provar suas propriedades.; The development of distributed systems and communication protocols is not a trivial task and the use of formal specification and verification techniques becomes necessary to assure the correctness of such systems. While model-checking techniques face the state space explosion problem...

Cardiovascular critical event pathways for the progression of heart failure; A report from the ATLAS study

Cleland, J.; Thygesen, K.; Uretsky, B.; Armstrong, P.; Horowitz, J.; Massie, B.; Packer, M.; Poole-Wilson, P.; Ryden, L.
Fonte: W B Saunders Co Ltd Publicador: W B Saunders Co Ltd
Tipo: Artigo de Revista Científica
Publicado em //2001 EN
Relevância na Pesquisa
45.77%
AIMS: To determine the sequence of critical cardiovascular events in the progression of heart failure, and whether aetiology or high-dose vs low-dose lisinopril affected these pathways. METHODS AND RESULTS: This was a post-hoc investigation of the ATLAS database, which comprised 3164 patients with chronic heart failure, randomized to low- (2.5-5.0 mg. day(-1)) or high-dose (32.5-35.0 mg. day(-1)) lisinopril, followed up for a median of 46 months. Two-thirds (64.3%) of patients had heart failure attributed to ischaemic heart disease. During the study, most patients (61.1%) had at least one cardiovascular hospitalization and 42.5% of all patients died: most deaths (88.2%) were cardiovascular. Nearly half (49.7%) of the cardiovascular deaths were considered sudden and 45.2% of cardiovascular deaths occurred as the first cardiovascular event. A third (30.2%) of deaths resulted from heart failure and were generally preceded by hospitalization, either for heart failure (85.5%), myocardial ischaemic events (21.7%) or arrhythmias (18.0%). Compared with low-dose, high-dose lisinopril was associated with a lower risk of death or hospitalization for any reason (P=0.002) and death or hospitalization with worsening heart failure (P<0.001). High-dose lisinopril delayed the time to all-cause mortality and hospitalization for chronic heart failure by 7.1 months. CONCLUSIONS: Vascular and arrhythmic events may not only be important precipitants of sudden death...

Especificación de patrones de diseño en event-B como procesos NTCC

Gómez Hernández, Carlos Eduardo
Fonte: Pontificia Universidad Javeriana; Facultad de Ingenieria; Carrera de Ingeniería de Sistemas y Computación Publicador: Pontificia Universidad Javeriana; Facultad de Ingenieria; Carrera de Ingeniería de Sistemas y Computación
Tipo: info:eu-repo/semantics/bachelorThesis; Trabajo de Grado; info:eu-repo/semantics/publishedVersion Formato: application/pdf; 65 p.
SPA
Relevância na Pesquisa
65.99%
Los métodos formales son importantes para modelar sistemas críticos, ya que con ellos se tiene una certeza del correcto funcionamiento de dichos sistemas. Por ejemplo, en el contexto de cirugías asistidas por computador, uno esperaría que cada acción del robot corresponda a la acción que el usuario (en este caso el doctor) esté realizando, después de todo, está en juego la vida de una persona. Dentro del diseño de software, Event-B usa modelos llamados patrones de diseño, y tal como se realiza en programación clásica, el reutilizar código es importante para hacer mejores programas y evitar pensar en problemas que previamente fueron resueltos. Event-B usa los patrones de diseño para reutilizar modelos que previamente han sido verificados, haciendo el proceso de modelamiento más eficiente. NTCC es un lenguaje concurrente que permite expresar de manera declarativa sincronización de procesos en diferentes unidades de tiempo. La idea general del proyecto es crear modelos de patrones de diseño en NTCC y proponer una forma de traducir dichos modelos a una estructura en Event-B. La manera para poderlo realizar es creando modelos generales de algunos patrones de diseño de dichos sistemas, modelarlos en ambos tipos de especifi- cación de sistemas...

Especificación de patrones de diseño en event-B como procesos NTCC

Gómez Hernández, Carlos Eduardo
Fonte: Carlos Eduardo Gómez Hernández Publicador: Carlos Eduardo Gómez Hernández
Tipo: info:eu-repo/semantics/workingPaper; Documento de trabajo; info:eu-repo/semantics/draft Formato: application/pdf; 5 p.
SPA
Relevância na Pesquisa
65.87%
Los métodos formales son importantes para modelar sistemas críticos, ya que con ellos se tiene una certeza del correcto funcionamiento de dichos sistemas. Por ejemplo, en el contexto de cirugías asistidas por computador, uno esperaría que cada acción del robot corresponda a la acción que el usuario (en este caso el doctor) esté realizando, después de todo, está en juego la vida de una persona. Dentro del diseño de software, Event-B usa modelos llamados patrones de diseño, y tal como se realiza en programación clásica, el reutilizar código es importante para hacer mejores programas y evitar pensar en problemas que previamente fueron resueltos. Event-B usa los patrones de diseño para reutilizar modelos que previamente han sido verificados, haciendo el proceso de modelamiento más eficiente. El proyecto de grado entonces explorará estos modelos, analizará sus semejanzas y propondrá un modelo de traducción entre modelos. Para realizarlo propondrá un lenguaje de alto nivel para que el diseñador le sea más sencillo especificar dichos patrones. Este lenguaje, como veremos, se puede traducir de manera simultánea a los dos tipos de especificaciones mencionados anteriormente manteniendo la estructura general del modelo que se quiere especificar. Así...

Model Checking Event-B by Encoding into Alloy

Matos, Paulo J.; Marques-Silva, Joao
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
45.91%
As systems become ever more complex, verification becomes more main stream. Event-B and Alloy are two formal specification languages based on fairly different methodologies. While Event-B uses theorem provers to prove that invariants hold for a given specification, Alloy uses a SAT-based model finder. In some settings, Event-B invariants may not be proved automatically, and so the often difficult step of interactive proof is required. One solution for this problem is to validate invariants with model checking. This work studies the encoding of Event-B machines and contexts to Alloy in order to perform temporal model checking with Alloy's SAT-based engine.

Abstract Data Types in Event-B - An Application of Generic Instantiation

Basin, David; Fürst, Andreas; Hoang, Thai Son; Miyazaki, Kunihiko; Sato, Naoto
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 26/10/2012
Relevância na Pesquisa
45.8%
Integrating formal methods into industrial practice is a challenging task. Often, different kinds of expertise are required within the same development. On the one hand, there are domain engineers who have specific knowledge of the system under development. On the other hand, there are formal methods experts who have experience in rigorously specifying and reasoning about formal systems. Coordination between these groups is important for taking advantage of their expertise. In this paper, we describe our approach of using generic instantiation to facilitate this coordination. In particular, generic instantiation enables a separation of concerns between the different parties involved in developing formal systems.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Proof Hints for Event-B

Hoang, Thai Son
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 06/11/2012
Relevância na Pesquisa
45.87%
Interactive proofs are often considered as costs of formal modelling activity. In an incremental development environment such as the Rodin platform for Event-B, information from proof attempts is important input for adapting the model. This paper considers the idea of using interactive proofs to "improve" the model, in particular, to convert them into automatic ones. We propose to lift some essential proof information from the interactive proofs into the model as what we called proof hints. In particular, proof hints are not only for the purpose of proofs: it helps to understand the formal models better.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Proceedings: Workshop on the experience of and advances in developing dependable systems in Event-B (DS-Event-B 2012)

Ishikawa, Fuyuki; Romanovsky, Alexander
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 09/11/2012
Relevância na Pesquisa
45.91%
These proceedings include papers presented at the Workshop on "The experience of and advances in developing dependable systems in Event-B" held on November 13, 2012 as part of the ICFEM 2012 (Kyoto, Japan).; Comment: Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements

Troubitsyna, Elena
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 25/10/2012
Relevância na Pesquisa
45.91%
Event-B has been actively used within the EU Deploy project to model dependable systems from various application domains. As a result, we have created a number of formal approaches to explicitly reason about dependability in the refinement process. In this paper we overview the work on formal engineering of dependable systems carried out in the Deploy project. We outline our approaches to integrating safety analysis into the development process, modelling fault tolerant systems and probabilistic dependability evaluation. We discuss achievements and challenges in development of dependable systems within the Event-B framework.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Development of Fault Tolerant MAS with Cooperative Error Recovery by Refinement in Event-B

Pereverzeva, Inna; Troubitsyna, Elena; Laibinis, Linas
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 25/10/2012
Relevância na Pesquisa
45.91%
Designing fault tolerance mechanisms for multi-agent systems is a notoriously difficult task. In this paper we present an approach to formal development of a fault tolerant multi-agent system by refinement in Event-B. We demonstrate how to formally specify cooperative error recovery and dynamic reconfiguration in Event-B. Moreover, we discuss how to express and verify essential properties of a fault tolerant multi-agent system while refining it. The approach is illustrated by a case study - a multi-robotic system.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Towards Refinement Strategy Planning for Event-B

Kobayashi, Tsutomu; Honiden, Shinichi
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 25/10/2012
Relevância na Pesquisa
45.99%
Event-B is a formal approach oriented to system modeling and analysis. It supports refinement mechanism that enables stepwise modeling and verification of a system. By using refinement, the complexity of verification can be spread and mitigated. In common development using Event-B, a specification written in a natural language is examined before modeling in order to plan the modeling and refinement strategy. After that, starting from a simple abstract model, concrete models in several different abstraction levels are constructed by gradually introducing complex structures and concepts. Although users of Event-B have to plan how to abstract the specification for the construction of each model, guidelines for such a planning have not been suggested. Specifically, some elements in a model often require that other elements are included in the model because of semantics constraints of Event-B. As such requirements introduces many elements at once, non-experts of Event-B often make refinement rough though rough refinement does not mitigate the complexity of verification well. In response to the problem, a method is proposed to plan what models are constructed in each abstraction level. The method calculates plans that mitigate the complexity well considering the semantics constraints of Event-B and the relationships between elements in a system.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B...

Formal Data Validation with Event-B

Badeau, Frédéric; Doche-Petit, Marielle
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 25/10/2012
Relevância na Pesquisa
45.82%
This article presents a verification and validation activity performed in an industrial context, to validate configuration data of a metro CBTC system by creating a formal B model of these configuration data and of their properties. A double tool chain is used to safely check whether a certain given input of configuration data fulfill its properties. One tool is based on some Rodin and open source plug-ins and the other tool is based on ProB.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B

Zhao, Yongwang; Yang, Zhibin; Sanan, David; Liu, Yang
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
45.85%
Standards play the key role in safety-critical systems. Errors in standards could mislead system developer's understanding and introduce bugs into system implementations. In this paper, we present an Event-B formalization and verification for the ARINC 653 standard, which provides a standardized interface between safety-critical real-time operating systems and application software, as well as a set of functionalities aimed to improve the safety and certification process of such safety-critical systems. The formalization is a complete model of ARINC 653, and provides a necessary foundation for the formal development and verification of ARINC 653 compliant operating systems and applications. Six hidden errors were discovered from the verification using the Event-B formal reasoning approach.; Comment: 12 pages

Managing LTL properties in Event-B refinement

Schneider, Steve; Treharne, Helen; Wehrheim, Heike; Williams, David
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
45.87%
Refinement in Event-B supports the development of systems via proof based step-wise refinement of events. This refinement approach ensures safety properties are preserved, but additional reasoning is required in order to establish liveness and fairness properties. In this paper we present results which allow a closer integration of two formal methods, Event-B and linear temporal logic. In particular we show how a class of temporal logic properties can carry through a refinement chain of machines. Refinement steps can include introduction of new events, event renaming and event splitting. We also identify a general liveness property that holds for the events of the initial system of a refinement chain. The approach will aid developers in enabling them to verify linear temporal logic properties at early stages of a development, knowing they will be preserved at later stages. We illustrate the results via a simple case study.

A Machine-Checked Proof for a Translation of Event-B Machines to JML

Cataño, Néstor; Rueda, Camilo; Wahls, Tim
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 09/09/2013
Relevância na Pesquisa
46.01%
We present a machine-checked soundness proof of a translation of Event-B to the Java Modeling Language (JML). The translation is based on an operator EventB2Jml that maps Evnet-B events to JML method specifications, and deterministic and non-deterministic assignments to JML method post-conditions. This translation has previously been implemented as the EventB2Jml tool. We adopted a taking our own medicine approach in the formalisation of our proof so that Event-B as well as JML are formalised in Event-B and the proof is discharged with the Rodin platform. Hence, for any Event-B substitution (whether an event or an assignment) and for the JML method specification obtained by applying EventB2Jml to the substitution, we prove that the semantics of the JML method specification is simulated by the semantics of the substitution. Therefore, the JML specification obtained as translation from the Event-B substitution is a refinement of the substitution. Our proof includes invariants and the standard Event-B initialising event, but it does not include full machines or Event-B contexts. We assume that the semantics of JML and Event-B operate both on the same initial and final states, and we justify our assumption.; Comment: 26 pages

A CSP Account of Event-B Refinement

Schneider, Steve; Treharne, Helen; Wehrheim, Heike
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 21/06/2011
Relevância na Pesquisa
45.95%
Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can moreover possibly be anticipated or convergent. All such steps are accompanied with precise proof obligations. Still, it remains unclear what the exact relationship - in terms of a behaviour-oriented semantics - between an Event-B machine and its refinement is. In this paper, we give a CSP account of Event-B refinement, with a treatment for the first time of splitting events and of anticipated events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement.; Comment: In Proceedings Refine 2011, arXiv:1106.3488

Event-B/SLP

Iliasov, Alexei
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 10/01/2013
Relevância na Pesquisa
45.89%
We show how the event-based notation offered by Event-B may be augmented by algorithmic modelling constructs without disrupting the refinement-based development process.; Comment: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012