ABZ'23

ABZ 2023 (Nancy, France)

9th International Conference on Rigorous State-Based Methods

A Framework for Formal Verification and Validation of Railway Systems

Abstract Railway systems belong to the domain of critical systems, where safety is a paramount concern. To ensure safety, testing methods have been implemented to adhere to certain standards. However, for large projects, it is impossible to test every possible scenarios, which can lead to gaps in the testing process.

Adding Records to Alloy

Abstract Records are a composite data type available in most programming and specification languages, but they are not natively supported by Alloy. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures.

AMAN Case Study

Abstract This document presents the case study for the ABZ 2023 conference. The case study introduces a safety critical interactive system called AMAN (Arrival MANager), which is a partly-autonomous scheduler of landing sequences of aircraft in airports.

Behavioural Theory of Reflective Algorithms

Abstract This “journal-first” paper presents a summary of the behavioural theory of reflective sequential algorithms (RSAs), i.e. sequential algorithms that can modify their own behaviour. The theory comprises a set of language-independent postulates defining the class of RSAs, an abstract machine model, and the proof that all RSAs are captured by this machine model.

Building Specifications in the Event-B Institution: A Summary

Abstract This “journal-first” paper summarises a publication by the same authors in the journal Logical Methods in Computer Science which describes a formal semantics for the Event-B specification language using the theory of institutions.

Crucible Tools for Test Generation and Animation of Alloy Models

Abstract Crucible is a suite of tools supporting the use of Alloy as a functional specification language for high-integrity software systems. It incorporates a test generator, animator and range of supporting tools.

Designing Critical Systems Using Hierarchical STPA and Event-B

Abstract In the design of critical systems, it is important to ensure a degree of formality so that we reason about safety and security at early stages of analysis and design, rather than detect problems later.

Encoding rmTLA+ Proof Obligations Safely for SMT

Abstract The (\textrm{TLA}^{+}) Proof System (TLAPS) allows users to verify proofs with the support of automated provers, including SMT solvers. To better ensure the soundness of TLAPS, we revisited the encoding of (\textrm{TLA}^{+}) into SMT-LIB, whose implementation had become too complex.

Exploration of Reflective ASMs for Security

Abstract We show how reflective ASMs can support hardware-software binding, which can be used for copy protection, and we exploit the logic of rASMs to express desirable properties for this application.

Exploring a Methodology for Formal Verification of Safety-Critical Systems

Abstract As the formal verification of safety-critical software systems often requires the integration of multiple tools and techniques, we propose a three-phase methodology incorporating two complementary workflows to ensure that the system in question fulfills its requirements.

Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems

Abstract The modeling language of classical B is used to write specifications of various systems. Tools like ProB are able to use modelchecking techniques to verify invariants of these specifications such as safety-properties.

formal MVC: A Pattern for the Integration of ASM Specifications in UI Development

Abstract Using architectural patterns is of paramount importance for guaranteeing the correct functionality, maintainability and modularity, especially for complex software systems. The model-view-controller (MVC) pattern is typically used in user interfaces (UIs), since it allows the separation between the internal representation of the information and the way it is shown to users.

Introducing Inductive Construction in B with the Theory Plugin

Abstract Proving theorems and properties on B models, recursively-defined functions is a convenient tool which is missing in B proofs. The main contribution of this paper is the definition of a new theory without new concrete types and without axioms to enable the use of constructions by induction; This theory has been specified and proved within the Theory Plugin in Rodin.

Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations

Abstract This paper presents insights gained during modeling and analyzing the arrival manager (AMAN) case study in Event-B with validation obligations (VOs). AMAN is a safety-critical interactive system for air traffic controllers to organize the landing of airplanes at airports.

Modeling and Verifying an Arrival Manager Using Event-B

Abstract The present paper describes an Event-B model of the Arrival MANager system (called AMAN), the case study provided by the ABZ’23 conference. The goal of this safety critical interactive system is to schedule the arrival times of aircraft at airports.

Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines

Abstract With the increasing complexity and scale of software-intensive systems, model-based system development requires composable system models and composition operators. In line with such a vision, this paper describes our experience in modeling the behavior of the MVM-Adapt, an adaptive version of the Mechanical Ventilator Milano that has been designed, certified, and deployed during the COVID-19 pandemic for treating pneumonia.

Modelling an Automotive Software System with TASTD

Abstract At the ABZ2020 Conference, the case study track proposed to model an Adaptive Exterior Light System and a Speed Control System: the former controls different exterior lights of a vehicle while the latter controls the speed of a vehicle.

Pattern-Based Refinement Generation Through Domain Specific Languages

Abstract The Event-B method is generally used to build models incrementally by integrating high level requirements. However, developing correct systems is not a cakewalk and remains a challenging task. In this paper, we focus on the preliminary steps of the development of safety-critical systems.

Reconstruction of TLAPS Proofs Solved by VeriT in Lambdapi

Abstract TLAPS, the TLA+ proof system [4], is a proof assistant for the development and mechanical verification of TLA(^+) proofs. Document If you cannot see the document below, the PDF document is most likely not freely accessible.

Refinements of Hybrid Dynamical Systems Logic

Abstract Hybrid dynamical systems describe the mixed discrete dynamics and continuous dynamics of cyber-physical systems such as aircraft, cars, trains, and robots. To justify correctness of their safety-critical controls for their physical models, differential dynamic logic ((\textsf {dL})) provides deductive specification and verification techniques implemented in the theorem prover KeYmaera X.

Standalone Event-B Models Analysis Relying on the EB4EB Meta-theory

Abstract Event-B is a state-based correct-by-construction system design formal method relying on proof and refinement where system models are expressed using set theory and First Order Logic (FOL). Through the generation and discharging of proof obligations (POs), Event-B natively supports the establishment of properties such as safety invariant, convergence and refinement.

Task Model Design and Analysis with Alloy

Abstract This paper describes a methodology for task model design and analysis using the Alloy Analyzer, a formal, declarative modeling tool. Our methodology leverages (1) a formalization of the HAMSTERS task modeling notation in Alloy and (2) a method for encoding a concrete task model and compose it with a model of the interactive system.

TASTD: A Real-Time Extension for ASTD

Abstract In ASTD, real-time models are not natively supported. Real-time requirements are pervasive in many systems, like control systems and cybersecurity. Timed Algebraic State Transition Diagrams (TASTD) is an extension of ASTD capable of specifying real-time models.

Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems

Abstract This paper presents a proof technique for proving refinements for general state-based models of concurrent systems that reduces proving forward simulations to thread-local, step-local proof obligations. Instances of this proof technique should be applicable to systems specified with ASM rules, B events, or Z operations.

Using Deep Ontologies in Formal Software Engineering

Abstract Isabelle/DOF is an ontology framework on top of Isabelle. It allows for the formal development of ontologies as well as continuous conformity-checking of integrated documents annotated by ontological data. An integrated document may contain text, code, definitions, proofs, and user-programmed constructs supporting a wide range of formal methods Isabelle/DOF is designed to leverage traceability in integrated documents by supporting navigation in Isabelle’s IDE as well as the document generation process.

Validation by Abstraction and Refinement

Abstract While refinement can help structure the modeling and proving process, it also forces the modeler to introduce features in a particular order. This means that features deeper in the refinement chain cannot be validated in isolation, making some reasoning unnecessarily intricate.

Validation of Formal Models by Interactive Simulation

Abstract Validating requirements for safety-critical systems with user interactions often involves techniques like animation, trace replay, and LTL model checking. However, animation and trace replay can be challenging since user and system events are not distinguished, and formulating LTL properties requires expertise.

Verifying Event-B Hybrid Models Using Cyclone

Abstract Modelling hybrid systems using Event-B is challenging and users typically are unsure about whether their Event-B models are over/under-specified. In this short paper, we present a work-in-progress specification language called Cyclone to tackle this challenge.

Verifying Temporal Relational Models with Pardinus

Abstract This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents (\textsf{Pardinus}), an extension of the popular (\textsf{Kodkod}) [12] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems.