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.
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.
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.
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.
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.
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.
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.
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.
Abstract Cloud computing technologies help developers build scalable distributed apps. Serverless architecture, or Function as a Service (FaaS), which separates app businesses into multiple functions, is one of the cloud-native architectures that has gained popularity.
Abstract The design of exception handling is a complex task requiring insight and domain expertise to ensure that potential abnormal conditions are identified and a recovery process is designed to return the system to a safe state.
Abstract The proof assistant Isabelle/HOL is made available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.
Abstract In the design of autonomous systems, seamless integration with human operators is crucial, particularly when humans are considered as a fail-safe for intervening in hazardous situations. This study presents an Event-B intervention timing pattern designed to include human drivers’ responses when they act as fallback mechanisms in Self-Driving Vehicle (SDV) systems.
Abstract ABZ and other state-based formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single language or tool emerging as the dominant solution for system design.
Abstract Apache Kafka is a distributed, fault-tolerant and highly available open-source technology that utilizes a publish-subscribe communication model to stream large volumes of data. It is widely being used in various domains such as finance, entertainment, online education, and e-commerce for real-time data processing and analytics.
Abstract Formal methods play a crucial role in modeling and quality assurance, but to be deployed on real systems, formal specifications need to be translated into implementation. Manually converting formal models into code poses challenges such as increased costs, limitations in specification reuse, and the potential for introducing errors.
Abstract B, Event-B and TLA+ are modelling notations based on set theory. Dedukti/Lambdapi is a logical framework based on the (\lambda \Pi )-calculus modulo rewriting in which many theories and logics can be expressed.
Abstract Refinement of Event-B machines is based on changing internal variables to obtain different data representations. One approach is expressed only in terms of internal variables. In the extreme case it permits refining a machine by another by choosing the gluing invariant “true”.
Abstract Transforming models based on their textual representation is a cumbersome task. This is particularly the case for Event-B, where the predominant representation is a set of XML files. As a consequence, tool support is lacking, even for minor refactoring operations.
Abstract Based on the logic of non-deterministic Abstract State Machines (ASMs) we define a modal extension (\mathcal{M}\mathcal{L}{\text {ASM}}) by first introducing multi-step predicates and then adding quantification over the number of steps.
Abstract A challenge posed by model-based formal methods such as Event-B is the validation of the models. This has been recognized and some tools have been created to provide modelers with means to animate models and to explore their behaviour through graphical display.
Abstract Abstract State Machines (ASMs) are widely used in the formalization and verification of the semantics of software or hardware. However, tools for assisting this process for evolving specifications are still lacking.
Abstract This paper introduces a novel approach to formal modelling and verification of ownership, addressing safety concerns in property transfer processes. The Event-B formal method, graphically represented using iUML-B notation, is used to establish a robust framework for modeling and verifying ownership systems.
Abstract The Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TiMo) or State Chart XML (SCXML). Typically, the syntactical elements of the languages are captured as Event-B contexts while the semantical elements are formalised in Event-B machines.
Abstract Previously, we introduced the idea of agile compiler development, i.e., starting from an initial compiler for the most simple program of a language and extending it in small versions, each introducing a new language concept.
Abstract This paper introduces the ABZ 2024 Case Study: Mechanical Lung Ventilator (MLV), inspired by the Mechanical Ventilator Milano developed during COVID-19. The case study reports the specification of the Mechanical Lung Ventilator used to ventilate patients who are not able to breathe on their own or need ventilation support.
Abstract The steep learning curve associated with interactive theorem proving poses a significant entry barrier for the learner. While the Alloy specification language [1] has simplified the introduction to and application of formal methods, transitioning to interactive theorem proving, such as with Coq [2], remains daunting due to the inherent complexity of formal reasoning and the sophisticated tooling required.
Abstract Petri-nets and their variants (Place/Transition nets, High-Level Petri Nets, etc.) are widely used in the development of safety critical-systems. Their success is related to three major aspects: a formal semantics, a graphical syntax and the availability of verification tools.
Abstract This paper introduces a transformation method that uses symbolic execution to eliminate sequential composition ((\texttt {seq})) rules from turbo ASM rules by translating them into equivalent rules without seq. Under some circumstances (\texttt {iterate}) rules can also be eliminated.