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. The presented model implements % implements ist mir etwas low-level human-machine interface comprising both interactive and autonomous parts. We employ VOs to formalize requirements, uncover contradictions and ambiguities, and validate the model's compliance with the requirements. To capture the AMAN's human-machine interaction, we implement an interactive domain-specific visualization and an automatic simulation using the VisB and SimB components of ProB.

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. The Analyzer then automatically verifies the overall model against desired properties, revealing counterexamples (if any) in terms of interaction scenarios between the operator and the system. In addition, we demonstrate how Alloy can be used to encode various types of operator errors (e.g., inserting or omitting an action) into the base HAMSTERS model and generate erroneous interaction scenarios. Our methodology is applied to a task model describing the interaction of a traffic air controller with a semi-autonomous Arrival MANager (AMAN) planning tool.

ABSTRACT. The present paper describes an Event-B model of the Arrival MANager system (called AMAN), the case study provided in the ABZ2023 conference. The goal of this safety critical interactive system is to schedule the arrival times of aircraft in airports. This system includes two parts: an autonomous part which predicts the arrival time of an aircraft from different information (flight plan information, radar and weather information, etc.) and an interface part that permits to the Air Traffic Controller (ATCo) to submit requests to AMAN like changes regarding the arrival times of aircraft. To formally model and verify such a critical system, we use a correct-by-construction approach with the Event-B method and its refinement process. We mainly consider functional features of the case study, all proof obligations have been discharged using the Rodin provers. Our model has been validated using ProB by applying scenarios related to different functional aspects of the system.

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. The main problem of using this approach in a formal setting, where formal models are used to specify the requirements and prove safety properties, is that those models are not directly used within the MVC pattern and, thus, all the activities performed at model-level are somehow lost when implementing the UI. For this reason, in this paper, we present the formal MVC pattern (fMVC), an extension of the classical MVC where the model is a formal specification, written using Abstract State Machines. This pattern is supported by the AsmetaFMVCLib, which allows the user to link the formal model with the view and the controller by using simple Java annotations. We present the application of fMVC on a simple example of a calculator for explanatory purposes, then we apply it to the AMAN case study, which has inspired the definition of fMVC. We discuss the advantages of fMVC and its shortcomings, trying to identify the scenarios where it should be applied and possible alternatives.

ABSTRACT. The VerCors verifier is a tool set for the verification of parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. In this talk I will first give an overview of the VerCors verifier, and how it  has been used for the verification of many different parallel and concurrent algorithms. In the second part of my talk I will zoom in on verification of GPU programs, as they are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. In my talk I introduce Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.

ABSTRACT. At ABZ 2020 Conference, the case study track demanded implementations of Adaptive Exterior Light System (ELS) and Speed Control System (SCS). ELS controls the different exterior lights of a vehicle; the SCS is the cruise control. This article introduces the TASTD model of the systems. Timed Algebraic State-Transition Diagrams (TASTD) is an extension of ASTD that adds time to its syntax and semantics. We have used ASTD modularisation to model the behaviour of different sensors and parts separately. ASTD orthogonality and ASTD operators let us join the pieces together. Our model considers all of both systems' requirements, including the ones with time management. We validate our implementation with the provided validation sequences. In ABZ 2020, several other solutions were presented, and we compare our approach to theirs. The advantages of having modularisation, orthogonality, abstraction, hierarchy, real-time, and graphical representation in one notation are highlighted with our implementation of the ABZ 2020 case study.

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. TASTD gives ASTD the capability to handle time with new algebraic operators. This paper describes the syntax and semantics of these new time op- erators: delay, persistent delay, timeout, persistent timeout, and timed interrupt. These new time operators are specified using two new operators, persistent guard and interrupt. To illustrate our extension, we present a small case study of a receiver sensor where we want to detect potential anomalies.

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. To exemplify the proof technique, we demonstrate it with a simple case study that verifies linearizability of a lock-free implementation of concurrent hash sets by showing that it refines an abstract concurrent system with atomic operations. Our theorem prover KIV translates programs to a set of transition rules and generates proof obligations according to the technique.

ABSTRACT. Today several high-level requirements languages are present on the market. Most of them have demonstrated great robustness in capturing, modeling, and verifying industrial requirements. However, developing these systems is not a cakewalk, especially in the context of big industrial projects [BDM98]. In this paper, we focus on the preliminary steps of the development of safety-critical systems. We investigate how patterns could be used in order to generate refinements automatically in the context of an Event-B development. Our main concerns are first to simplify the development of such systems by the use of patterns, and second to produce Event-B machines such that the user can choose to refine them additionally.

ABSTRACT. With the increasing complexity and scale of software-intensive systems, model-based system development requires composable system models and composition of their analysis. Consequently, to design and reason about behavior and quality of a system it is necessary to develop separate models of the system's subsystems/components, which must be subsequently combined to analyze the overall behavior and quality of the system under prototyping. In line to such a vision, this paper describes our experience in modeling and validating the behavior of MVM-Adapt, an adaptive version of the Mechanical Ventilator Milano that has been designed, certified, and deployed during the COVID-19 pandemic. To keep the complexity of the requirements and models under control, we exploited a compositional modeling and validation technique for discrete-event systems based on Abstract State Machines (ASMs). Essentially, separate ASMs represent the behavior of independent and interacting subsystems of the MVM with their new adaptive functionalities, and can communicate to each other through I/O events. These ASM models have been developed, validated, and verified separately. An orchestrated simulation coordinates the overall execution of these communicating I/O ASMs by exploiting typical workflow patterns like parallel composition and cascading. This compositional simulation technique has proved to be very useful in practice for a fast and reliable prototyping of the new adaptive behavior of the MVM.