Workshop on B Dissemination [WOBD]

Evénement satellite de SBMF 2010

8-9 Novembre 2010, Natal, Brésil

Programme

Jour 1

Refinement in UML-B

UML-B is a UML-like graphical drawing tool for the Event-B language. It includes Class diagrams and State machines which add convenient mechanisms for structuring models and sequencing events. This talk will explain refinement in UML-B models. In particular, the talk will explore how these additional notational constructs work with refinement and illustrate the use of features built into UML-B in order to express refinement diagrammatically.

ProB for Animation, Model Checking and Constraint Solving : Michael Leuschel (University of Dusseldorf)

We present the animator and model checker ProB. We discuss recent developments and give hints on how to write specifications which can be more efficiently validated (e.g., using symmetry reduction). We also show the constraint solving capabilities of ProB, and illustrate how one can use B and ProB as a convenient constraint solving environment.

Potpourri of what ? One year in a DA's life: Aryldo G. Russo Jr., Thiago C. de Sousa, Haniel Barbosa (AeS Group), Paulo Muniz (University of Sao Paulo), David Déharbe (University of Rio Grande do Norte)

This talk presents a collection of what we have been doing so far in the context of DEPLOY Associate program. Besides the progress of the pilot project, the development of a speci fication of a simple railway system called "dead man control", we also present some parallel developments, some theorical, some practical of the use of formal methods in industry. As the space is restrict, we present only some superfi cial information about what we are doing in these di fferent but convergent projects.

Deployment in business information software : Andreas Roth (SAP, Germany), Thierry Lecomte (ClearSy, France)

This talk presents the pilot deployment in the sector of business information systems which takes place within the Deploy project. Special emphasis in this deployment is put on the integration of formal modeling with existing domain-specific modeling languages in the business information domain. As first result we describe the integration of Event-B with service choreography models.

Validation of Railway Properties with ProB : Michael Leuschel (University of Dusseldorf)

We present our successful applications of ProB to validate properties of railway topologies within Siemens, notably for the metro lines in San Juan, Sao Paolo, Paris (Line 1) and Barcelona. We discuss the underlying techniques that made the validation possible, and present a tutorial on validating properties about large constants with ProB.

Evaluating a control system architecture based on a formally derived AOCS model

Jour 2

Proving Reachability in B using Substitution Refinement : Marc Frappier, Amel Mammar and Fama Diagne

This paper proposes an approach to prove reachability properties of the form AG psi => EF phi using substitution refinement in classical B. Such properties denote that there exists an execution path for each state satisfying psi to a state satisfying phi. These properties frequently occur in security policies and information systems. We show how to use Morgan's specification statement to represent a property and refinement laws to prove it. The idea is to construct by stepwise refinement a program whose elementary statements are operation calls. Thus, the execution of such a program provides an execution satisfying AG psi => EF phi. Proof obligations are represented using assertions (ASSERT clause of B) and can be discharged using Atelier B.

A Proof-Based Approach to Verifying Reachability Properties : Amel Mammar, Fama Diagne and Marc Frappier

This paper presents a formal approach to proving temporal reachability properties, expressed in CTL, on B systems. We are particularly interested in demonstrating that a system can reach a given state by executing a sequence of actions or operations called a path. Starting with a path, the proposed approach consists in calculating the proof obligations to discharge in order to prove that the path allows the system to evolve in order to verify the desired property. Since these proof obligations are expressed as first logic formulas without any temporal operator, they can be achieved using the prover of AtelierB. Our proposal is illustrated through a case study.

Integrating Rodin with SMT-Solvers : Vítor Alcântara and David Déharbe

Formal developments such as modelling and refinement in Event-B generate a large amount of proof obligations. SMT-solvers are a new family of theorem provers that hold the promise of not only automation and speed, but also additional features such as proof and counter-model generation. This paper presents a plug-in created to integrate SMT-Solvers in the Rodin platform, so the user can make fast and automatic use of these two platforms together. This plug-in implements a translation from the proof obligations generated in Rodin to the SMT-LIB format, calls a SMT-Solver on the results of this translation, and returns the result of proof immediately to Rodin.

B for Real : Thierry Lecomte

This paper presents preliminary work on introducing real numbers and floating point numbers (IEEE 754) in B, in order to be able to model software manipulating such numbers. Modifications of the language and the target tool (Atelier B) are identified and justified. An example is used all along the presentation to demonstrate the approach.

Modularisation in Event-B : Alexei Iliasov (Newcastle University, UK)

The talk will present a novel composition/decomposition approach developed for the Event-B method. It is based on introducing the concepts of modules and module interfaces, and relies on machine decomposition using the intuitive operation call metaphor. The talk will describe the motivations for introducing the approach and demonstrate its soundness. We will introduce the modularisation plugin supporting modularisation within the Rodin Toolkit and show a brief demo. Some common patterns of model structuring will be discussed and illustrated with a case study. We will report on a substantial development of an industrial midium-scale application from the aerospace domain, in which the modularisation approach has been extensively used. This work is a result of collaboration between Newcastle University, Abo Akademy and Space Systems Finland within the ICT DEPLOY Integrated Project. More information can be found at http://wiki.event-b.org/index.php/Modularisation_Plug-in.

A Methodological WRSPM Approach to a B Formalization in an Industrial Setting : Haniel Barbosa, Aryldo G. Russo Jr., and David Déharbe

Requirements are often expressed in a natural language. Building a formal model of such requirements is still an open issue in software development. We propose a systematic approach to understand and organize requirements so that the construction of a formal speci cation is facilitated. We present an intermediate model that stands between the natural language requirements and the abstract model for the functional speci cation. This intermediate model facilitates traceability between the different artifacts produced in the software development process, which is a requirement for ful lling international safety standards. Subsequently we present and analyze the results of trying to produce a formal speci cation from this intermediate model incrementally, along with descriptions and alternative solutions to the complications we faced. We present the application of this method to the requirements of a real public transportation system.

From system to software : Thierry Lecomte (ClearSy)

We present a complete path from Rodin system-level models to Atelier B software models, exhibiting a modelling and development process allowing to use the best of the two platforms while specifying, refining and implementing systems and software.