Abstract In this paper, we present a formal Event-B model of the Mechanical Lung Ventilator (MLV), the case study provided by the ABZ’24 conference. This system aims at helping patients maintain good breathing by providing mechanical ventilation. For this purpose, two modes are possible: Pressure Controlled Ventilation (PCV) and Pressure Support Ventilation (PSV). In the former mode, respiratory cycles are completely defined by the patient that is able to start breathing on its own. In the latter mode, the respiratory cycle is constant and controlled by the ventilator. Let us note that it is possible to move from a given mode to the other depending on the breathing capabilities of the patient under ventilation. In this paper, we illustrate the use of a correct-by-construction approach, the Event-B formal method and its refinement process, for the formal modeling and the verification of such a complex and critical system. The development of the formal models has been achieved under the Rodin platform that provides us with automatic and interactive provers used to verify the correctness of the models. We have also validated the built Event-B models using the ProB animator/model checker.
Abstract In this paper, we use NASA’s Formal Requirements Elicitation Tool (FRET) and the Event-B formal method to model and verify the requirements for the ABZ 2024 case study which is a mechanical lung ventilator. We use the FRET requirements to guide the development of a formal design model in Event-B. We provide details about the artefacts produced and reflect on our experience of using these tools in this case study. We focus on the functional and controller requirements for this system, as given in the case study documentation. This paper provides a first step towards using Event-B as part of a FRET-guided verification workflow in a large case study.
Abstract We model the Mechanical Lung Ventilator (MLV) in the process algebra mCRL2. The functional requirements of the MLV are formalised in the modal mu-calculus, and we use model checking to analyse whether these requirements hold true of our model. Our formalisation of the MLV and its requirements reveal a few subtle imprecisions and unclarities in the informal document and we analyse their impact.
Abstract For the ABZ2024 conference, the proposed case study consists of modelling the adaptive outdoor mechanical lung ventilation system. The mechanical lung ventilator is intended to provide ventilation support for patients that are in intensive therapy and that require mechanical ventilation. The system under study is made up of two main software components: the graphical user interface (GUI) and the controller, this paper introduces a model for the controller part of the software system using Timed Algebraic State-Transition Diagrams (TASTD). TASTD is an extension of Algebraic State-Transition Diagrams (ASTD) providing timing operators to express timing constraints. The specification makes extensive use of the TASTD modularity capabilities, thanks to its algebraic approach, to model the behaviour of different sensors and actuators separately. We validate our specification using the cASTD compiler, which translates the TASTD specification into a C++ program. This generated program can be executed in simulation mode to manually update the system clock to check timing constraints. The model is executed on the test sequences provided with the case study. The advantages of having modularisation, orthogonality, abstraction, hierarchy, real-time, and graphical representation in one notation are highlighted with the proposed model.
Abstract This case-study paper reports on our experience in modelling the mechanical lung ventilator using the Clock Constraint Specification Language (CCSL). CCSL captures the causal and temporal behaviour of a system by specifying constraints on logical clocks. Logical clocks are integer counters where the occurrence of an event, a tick, advances the counter and marks the advance in time. In this framework, chronometric clocks become logical clocks just with a special external meaning. Encoding chronometric clocks as counters may result in verification inefficiency and hard-to-read specifications. The paper introduces in the language some real-time constructs to directly encode phenomena like clock drift, skew and jitter. This makes patterns explicit in turn enabling optimizations. To realize these optimizations, we alter the internal symbolic representation of clock constraints. We also introduce an explicit notion of parameters and intervals. While for some constraints it mainly consists of adding syntactic sugar and pre-processing facilities, we believe it improves the readability. We illustrate the new constructs on the mechanical lung ventilator system. We start with a purely logical specification, we point at the sources of inefficiencies and then we discuss the benefits of the extensions on specific parts.
Abstract We propose a definition of a class of reflective Abstract State Machines (ASMs) that extends the class of Parallel Guarded Assignments (PGAs), a subclass of single-agent sequential ASMs, and can serve as ground model for refinements of reflectivity in concrete programming languages.
Abstract Blockchain has shown to be a versatile technology with applications ranging from financial services and supply chain management to healthcare, identity verification, etc. Thanks to the usage of smart contracts, blockchain can streamline and automate complex processes, eliminating the need for intermediaries and reducing administrative overhead. Smart contracts often handle valuable assets and execute critical functions, making them attractive targets for attackers. Thus, secure and reliable smart contracts are necessary. The long-term research we present aims to face the problem of safety and security assurance of smart contracts at design time. We are investigating the usage of the Abstract State Machine (ASM) formal method for the specification, validation, and verification of Ethereum smart contracts. We provide (i) a set of ASM libraries that simplify smart contracts modeling, (ii) models of malicious contracts to be used to check the robustness of a contract against some given attacks, (iii) patterns of properties to be checked to guarantee the operational correctness of the contract and its adherence to certain predefined properties.
Abstract Humans are good at understanding subjective or vague statements which, however, are hard to express in classical logic. Fuzzy logic is an evolution of classical logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers.This paper shows how a model checker such as Alloy can evolve to handle both classical and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.
Abstract The use of SAT-based model finding for specification analysis is a crucial characteristic of Alloy, and a main reason of its success as a language for software specification. When a property of a specification is analyzed and deemed satisfiable, the user usually explores instances of the corresponding satisfiability, in order to understand the analysis outcome. The order in which instances are obtained during exploration can impact the efficiency and effectiveness with which specification analysis is carried out. This has been observed by various researchers, and different instance exploration strategies have been proposed, besides the standard SAT-solver driven strategy implemented with the Alloy Analyzer. In this paper, we concentrate on a strategy recently proposed in the literature, that we refer to as “field-value” driven, and has been implemented in the tool HawkEye. The tool allows the user to interactively guide instance exploration, by enforcing constraints requiring fields to contain (resp., do not contain) specific values. We design an experiment involving faulty Alloy specifications featuring combinations of over constraints and under constraints, and perform a user study to analyze the impact of this instance exploration strategy, in comparison with the standard SAT-solver driven exploration. The study focuses on HawkEye’s facility of interactive instance querying and how it may favor users, in its current realization, during Alloy model analysis and debugging. We perform an assessment of the evaluation, and summarize some of the reasons that may diminish the impact of field-value exploration in model finding.