Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2016, held in Linz, Austria, in May 2016.
The 17 full and 15 short papers presented in this volume were carefully reviewed and selected from 61 submissions. They record the latest research developments in state-based formal methods Abstract State Machines, Alloy, B, Circus, Event-B, TLS+, VDM and Z.

Inhaltsverzeichnis

Frontmatter

Keynote Article

Frontmatter

Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets

We show how to model distributed algorithms by Abstract State Machines (ASMs). Comparing these models with Petri nets (PNs) reveals a certain number of idiosyncrasies of PNs which complicate both model design and analysis. The ASMs we define illustrate how one can avoid such framework related technicalities.

Egon Börger

Regular Research Articles

Frontmatter

A Universal Control Construct for Abstract State Machines

Abstract State Machines can be used to specify arbitrary system behaviour. However, when writing executable specifications one often has to write additional statements which organise how, e.g., in which order, the rules are executed. This reduces the readability and comprehensibility of specifications and can introduce additional defects to them. We propose a new syntax construct for the specification of control flow for the ASM language which improves the compactness and readability of specifications by providing syntactic elements for often manually realised behaviour. This construct enables to parametrise which rules shall be selected for execution and how the selected rules are executed. We illustrate how the control construct can improve the code’s readability on some examples. The proposed control construct is also released as a plugin for CoreASM.

Michael Stegmaier, Marcel Dausend, Alexander Raschke, Matthias Tichy

Encoding TLA into Many-Sorted First-Order Logic

This paper presents an encoding of a non-temporal fragment of the $${\textsc {TLA}} ^{{+}}$$TLA+ language, which includes untyped set theory, functions, arithmetic expressions, and Hilbert’s $$\varepsilon $$ε operator, into many-sorted first-order logic, the input language of state-of-the-art smt solvers. This translation, based on encoding techniques such as boolification, injection of unsorted expressions into sorted languages, term rewriting, and abstraction, is the core component of a back-end prover based on smt solvers for the $${\textsc {TLA}} ^{{+}}$$TLA+ Proof System.

Stephan Merz, Hernán Vanzetto

Proving Determinacy of the PharOS Real-Time Operating System

Executions in the PharOS real-time system are deterministic in the sense that the sequence of local states for every process is independent of the order in which processes are scheduled. The essential ingredient for achieving this property is that a temporal window of execution is associated with every instruction. Messages become visible to receiving processes only after the time window of the sending message has elapsed. We present a high-level model of PharOS in TLA+ and formally state and prove determinacy using the TLA+ Proof System.

Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz

A Rigorous Correctness Proof for Pastry

Peer-to-peer protocols for maintaining distributed hash tables, such as Pastry or Chord, have become popular for a class of Internet applications. While such protocols promise certain properties concerning correctness and performance, verification attempts using formal methods invariably discover border cases that violate some of those guarantees. Tianxiang Lu reported correctness problems in published versions of Pastry and also developed a model, which he called LuPastry, for which he provided a partial proof of correct delivery assuming no node departures, mechanized in the TLA$$^+$$+ Proof System. Lu’s proof is based on certain assumptions that were left unproven. We found counter-examples to several of these assumptions. In this paper, we present a revised model and rigorous proof of correct delivery, which we call LuPastry$$^+$$+. Aside from being the first complete proof, LuPastry$$^+$$+ also improves upon Lu’s work by reformulating parts of the specification in such a way that the reasoning complexity is confined to a small part of the proof.

Noran Azmy, Stephan Merz, Christoph Weidenbach

Enabling Analysis for Event-B

In this paper we present a static analysis to determine how events influence each other in Event-B models. The analysis, called an enabling analysis, uses syntactic and constraint-based techniques to compute the effect of executing one event on the guards of another event. We describe the foundations of the approach along with the realisation in ProB. The output of the analysis can help a user to understand the control flow of a formal model. Additionally, we discuss how the information of the enabling analysis can be used to obtain a new optimised model checking algorithm. We evaluate both the performance of the enabling analysis and the new model checking technique on a variety of models. The technique is also applicable to B, $$\mathrm{TLA}^{+}$$TLA+, and Z models.

Ivaylo Dobrikov, Michael Leuschel

A Compact Encoding of Sequential ASMs in Event-B

We present a translation of sequential ASMs to Event-B specifications. The translation also addresses the partial update problem, and allows a variable to be updated (consistently) in parallel. On the theoretical side, the translation highlights the intricacies of ASM rule execution in terms of Event-B semantics. On the practical side, we show on a series of examples that the Event-B encoding remains compact and is amenable to proof within Rodin as well as animation and model checking using ProB.

Michael Leuschel, Egon Börger

Proof Assisted Symbolic Model Checking for B and Event-B

We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature of B and Event-B accounts for complicated constraints arising in these symbolic analysis techniques. In this paper we suggest using static information stemming from proof obligations to simplify occurring constraints. We show how to include proof information in the aforementioned algorithms. Using different benchmarks we compare explicit state to symbolic model checking as well as techniques with and without proof assistance. In particular for models with large branching factor, e.g., due to complicated data values being manipulated, the symbolic techniques fare much better than explicit state model checking. The inclusion of proof information results in further clear performance improvements.

Sebastian Krings, Michael Leuschel

On Component-Based Reuse for Event-B

Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by a component-based reuse strategy. In this paper, we outline a component-based reuse methodology for Event-B. It provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We describe the process of creating library components, their composition, and specification of new properties (involving the composed elements). We introduce Event-B component interfaces and propose to use a diagrammatic representation of component instances (based on iUML-B) which can be used to describe the relationships between the composed elements. We also discuss the specification of communication flow across component boundaries and describe the additional proof obligations that are required.

Andrew Edmunds, Colin Snook, Marina Walden

Using B and ProB for Data Validation Projects

Constraint satisfaction and data validation problems can be expressed very elegantly in state-based formal methods such as B. However, is B suited for developing larger applications and are there existing tools that scale for these projects? In this paper, we present our experiences on two real-world data validation projects from different domains which are based on the B language and use ProB as the central validation tool. The first project is the validation of university timetables, and the second project is the validation of railway topologies. Based on these two projects, we present a general structure of a data validation project in B and outline common challenges along with various solutions. We also discuss possible evolutions of the B language to make it (even) more suitable for such projects.

Dominik Hansen, David Schneider, Michael Leuschel

Generating Event-B Specifications from Algorithm Descriptions

We present a high-level algorithm description language which is translated to Event-B specifications for simulation, model checking and proof. Rather than trying to recover the program structure from a lower-level Event-B specification, we start with a high-level description of the algorithm. Our goals are more tractable code generation and more convenient modelling, while keeping the power of the Event-B method in terms of proof and refinement. We present various examples of algorithm descriptions and show that our translation ensures that they can be completely proven within Rodin while achieving a high-level of automatic proof.

Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel

Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions

In this paper, we propose a formal framework enhancing the termination detection property of distributed algorithms and reusing their specifications as well as their proofs. By relying on refinement and composition, we show that an algorithm specified with local termination detection, can be reused in order to compute the same algorithm with global termination detection. The main idea relies upon the development of distributed algorithms following a top/down approach and the integration of additional computation steps developed in a pre-defined module. This module is specified in a generic and scalable way in order to be composed with particular developments. Once the composition link is proven, the global termination emerges automatically.

Maha Boussabbeh, Mohamed Tounsi, Mohamed Mosbah, Ahmed Hadj Kacem

How to Select the Suitable Formal Method for an Industrial Application: A Survey

The share of formal methods is still marginal in contemporary systems and software engineering. One of the reasons is the absence of systematic guidelines and evaluation criteria that help software practitioners choose the right formal method for the problem at hand. In this paper, we present a comprehensive set of criteria, based on a systematic literature review and decade-long personal experience in industrial projects, for evaluating and comparing different formal methods. We argue that besides technical grounds (e.g., modeling capabilities and supported development phases), formal methods should also be evaluated from social and industrial perspectives. At the end of the paper, we present an evaluation of “ABZ” methods based on the stipulated criteria.

Felix Kossak, Atif Mashkoor

Short Articles (Work in Progress)

Frontmatter

Unified Syntax for Abstract State Machines

The paper presents our efforts in defining UASM, a unified syntax for Abstract State Machines (ASMs), based on the syntaxes of two of the main ASM frameworks, CoreASM and ASMETA, which have been adapted to accept UASM as input syntax of all their validation and verification tools.

Paolo Arcaini, Silvia Bonfanti, Marcel Dausend, Angelo Gargantini, Atif Mashkoor, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra, Michael Stegmaier

A Relational Encoding for a Clash-Free Subset of ASMs

This paper defines a static check for clash-freedom of ASM rules, including sequential and parallel composition, nondeterministic choice, and recursion. The check computes a formula that, if provable, makes a relational encoding of ASM rules possible, which is an important prerequisite for efficient deduction. The check is general enough to cover all sequential rules as well as many typical uses of parallel composition.

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif

Towards an ASM Thesis for Reflective Sequential Algorithms

Starting from Gurevich’s thesis for sequential algorithms (the so-called “sequential ASM thesis”), we propose a characterization of the behaviour of sequential algorithms enriched with reflection. That is, we present a set of postulates which we conjecture capture the fundamental properties of reflective sequential algorithms (RSAs). Then we look at the plausibility of an ASM thesis for the class of RSAs, defining a model of abstract state machine (which we call reflective ASM) that we conjecture captures the class of RSAs as defined by our postulates.

Flavio Ferrarotti, Loredana Tec, José María Turull Torres

A Model-Based Transformation Approach to Reuse and Retarget CASM Specifications

The Abstract State Machine (ASM) theory is a way to specify algorithms, applications and systems in a formal model. Recent ASM languages and tools address either the translation of ASM specifications to a specific target programming language or aim at the execution in a specific environment. In this work-in-progress paper we outline a model-based transformation approach supporting (1) the specification of applications or systems using the Corinthian Abstract State Machine (CASM) modeling language and (2) retargeting those applications to different programming language and hardware target domains. An intermediate model is introduced, which not only captures software-based implementations, but also the generation of hardware-related code in the same model. This approach offers a new formal modeling perspective onto modular, reusable and retargetable software and hardware designs for the development of embedded systems. We provide a short overview of our CASM compiler design as well as the retargetable model-based approach to generate code for different target domains.

Philipp Paulweber, Uwe Zdun

Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy

We describe an Alloy model that helps check the correctness of a discrete wet-dry algorithm used in a system for hurricane storm surge prediction. Derived from simplified physics and encoded with empirical rules, the algorithm operates on a finite element mesh to allow the propagation of overland flows. Our study is motivated by complex interactions between the algorithm and a recent performance enhancement to the system that involves mesh partitioning. We briefly outline our approach and describe safety properties of the extension, as well as directions for future work.

John Baugh, Alper Altuntas

‘The Tinker’ for Rodin

PSGraph [3] is a graphical proof strategy language, which uses the formalisation of labelled hierarchical graphs to provide support for the development and maintenance of large and complex proof tactics. PSGraph has been implemented as the Tinker system, which previously supported the Isabelle and ProofPower theorem provers [4]. In this paper we present a Rodin version of Tinker, which allows Rodin users to encode, analyse and debug their proof strategies in Tinker.

Yibo Liang, Yuhui Lin, Gudmund Grov

A Graphical Tool for Event Refinement Structures in Event-B

The Event Refinement Structures (ERS) approach provides a graphical extension of the Event-B formal method to represent event decomposition and control-flow explicitly. In this paper we present an improved version of the ERS plug-in, which provides a graphical environment for the ERS approach within the Event-B tool, Rodin. The improved ERS plug-in is based on the available frameworks that are developed to support Event-B with an EMF framework, language extensions and generic diagram extensions.

Dana Dghaym, Matheus Garay Trindade, Michael Butler, Asieh Salehi Fathabadi

Rodin Platform Why3 Plug-In

We briefly present the motivation, architecture and usage experience as well as proof statistics for a new Rodin Platform proof back-end based on the Why3 umbrella prover. Why3 offers a simple and versatile notation as a common interface to a large number of automated provers including all the leading SMT-LIB and TPTP compliant tools. The plug-in can function either in a local mode when all the provers are installed locally, or remotely as a cloud service. We discuss the experience of building the tool, the current status and the potential advantages of a cloud-hosted proof infrastructure.

Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander Romanovsky

Semi-Automated Design Space Exploration for Formal Modelling

Refinement based formal methods allow the modelling of systems through incremental steps via abstraction. Discovering the right levels of abstraction, formulating correct and meaningful invariants, and analysing faulty models are some of the challenges faced when using this technique. We propose Design Space Exploration that aims to assist a designer by automatically providing high-level modelling guidance.

Gudmund Grov, Andrew Ireland, Maria Teresa Llano, Peter Kovacs, Simon Colton, Jeremy Gow

Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development

This paper presents a substitution mechanism for systems having a continuous behavior. It shall preserve the safety property stating that the output of both systems remain in a safety envelope. The whole approach is formalized using Event-B, and relies on the Rodin tools and a theory of Reals provided by the Rodin Theory Plug-in to check the internal consistency with respect to safety properties, invariants and events.

Guillaume Babin, Yamine Aït-Ameur, Neeraj Kumar Singh, Marc Pantel

UC-B: Use Case Modelling with Event-B

Use cases are a popular but informal technique used to define and analyse system behaviour. We introduce UC-B a plug-in for the Rodin platform (Event-B tool) that supports the authoring and management of use case specifications with both informal and formal components. The formal component is based on Event-B’s mathematical language. Once the behaviour of the use case is specified, UC-B automatically generates a corresponding Event-B model. The resulting model is then amenable to the Rodin verification tools that enable system level properties to be verified. By underpinning informal use case modelling with Event-B we are able to provide greater precision and formal assurance during the early stages of design.

Rajiv Murali, Andrew Ireland, Gudmund Grov

Interactive Model Repair by Synthesis

When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, deadlocks or refinement errors. Errors are presented as counter-example states and traces and should help fixing the underlying bugs. We suggest automating parts of this process: Using a synthesis technique, we try to generate more permissive or restrictive guards or invariants. Furthermore, synthesized actions allow to modify the behaviour of the model. All this could be done with constant user feedback, yielding an interactive debugging aid.

Joshua Schmidt, Sebastian Krings, Michael Leuschel

SysML2B: Automatic Tool for B Project Graphical Architecture Design Using SysML

We present an approach to transform SysML structural diagrams, BDD and IBD with constraints, into a B Method project skeleton. This project can then be directly used for implementation development through usual B refinement mechanism. We prototyped this approach.

David Mentré

Mechanized Refinement of Communication Models with TLA

In distributed systems, asynchronous communication is often viewed as a whole whereas there are actually many different interaction protocols whose properties are involved in the compatibility of peer compositions. A hierarchy of asynchronous communication models, based on refinements, is established and proven with the TLA $$^+$$ + Proof System. The work serves as a first step in the study of the substituability of the communication models when it comes to compatibility checking.

Florent Chevrou, Aurélie Hurault, Philippe Mauran, Philippe Quéinnec

A Super Industrial Application of PSGraph

The ClawZ toolset has been successful in verifying that Ada code is correctly generated from Simulink models in an industrial setting, using the Z notation. D-RisQ is now extending this technique to new domains of the C programming language, which requires changes to their highly complex proof technique. In this paper, we present initial results in the technology transfer of the graphical PSGraph language to support this extension, and show feasibility of PSGraph for industrial use with strong maintainability requirements.

Yuhui Lin, Gudmund Grov, Colin O’Halloran, Priiya G.

Articles Contributing to the Hemodialysis Machine Case Study

Frontmatter

The Hemodialysis Machine Case Study

This documents presents a description of a case study concerning the control of a hemodialysis (HD) machine. It provides an overview of the requirements and the design of an HD machine including a sketch of the machine’s functionality, related safety conditions, and a top-level system architectural description.

Atif Mashkoor

How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study

Medical devices are nowadays more and more software dependent, and software malfunctioning can lead to injuries or death for patients. Several standards have been proposed for the development and the validation of medical devices, but they establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability.This paper takes advantage of the Hemodialysis machine case study to present a formal development process supporting most of the engineering activities required by the standards, and provides rigorous approaches for system validation and verification. The process is based on the Abstract State Machine formal method and its model refinement principle.

Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene

Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation

We present a formal specification of a hemodialysis machine (HD machine) using Event-B. We model the HD machine using iUML-B state-machines and class diagrams and build a corresponding BMotion Studio visualisation. We focus on validation using (i) diagrams to aid the modelling of the sequential properties of the requirements, and (ii) ProB-based animation and visualisation tools to explore the system’s behaviour. Some of the safety properties involve dynamic behaviour which is difficult to verify in Event-B. For these properties we use co-simulation tools to validate against a continuous model of the physical behaviour.

Thai Son Hoang, Colin Snook, Lukas Ladenberger, Michael Butler

Hemodialysis Machine in Hybrid Event-B

The hemodialysis machine case study is examined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A broadly component based strategy is adopted, using the multi-machine and coordination facilities of Hybrid Event-B. Since, like most medical procedures, hemodialysis is under overall human control, it is largely a sequential process, with some branching to deal with exceptional circumstances. This makes for a relatively uncomplicated modelling framework, provided a model of the operator is included in order to capture the handling of exceptions.

Richard Banach

Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods

This paper presents the specification of the hemodialysis case study, proposed by ABZ’16 conference. The specification was carried out by a coupling of Algebraic State-Transition Diagrams (astd) and B-like methods. astd are a graphical notation, based on automata and process algebra operators. They provide an easy-to-read specification of the dynamic behaviour of the system. The data model is specified using the Event-B language. The system is incrementally designed using extended refinement of both methods.

Thomas Fayolle, Marc Frappier, Frédéric Gervais, Régine Laleau

Modelling the Haemodialysis Machine with Circus

We present a formal model of aspects of the haemodialysis machine case study using the Circus specification notation. We focus on building a model in which each of the software requirements (R-1–36) are represented by a Circus action. All of these act in concert with actions that model the collection of sensor data and the progress through the various therapy phases and activities. We then present how we model check the system using FDR.

Artur O. Gomes, Andrew Butterfield

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise