While detection of suspicious or erroneous CPU behaviour can be achieved by generic mechanisms such as memory-safe processors, recovering safely from the resulting exceptions is an application-specific problem. The challenge is to ensure that a complex closed system including the controller and its environment remain in a safe state while undertaking abnormal state changes in the controller as part of its exception recovery process. Handling exceptional error events is a complex task that requires insight and domain expertise to ensure that a process is designed to recover from abnormal conditions and return the system to a safe state. Exception handling relies on a notion of transactions in order to identify how the system can be systematically returned to a consistent state. Formal methods can address this complexity, by supporting the analysis of transactions and exception handling at the abstract design stages utilising mathematical modelling and proofs. Event-B is a state-based formal method for modelling and verifying the consistency of discrete systems; however, it lacks explicit support for analysing the handling of exceptions. UML-B is a diagrammatic front-end for Event-B modelling which allows models to be constructed using class diagrams and state machines. In this paper, we use UML-B state machines to support the modelling of normal behaviour, with a notion of consistency and augment this with a technique for modelling 'transactions' which may either complete to reach a consistent state or encounter exceptional errors that have to return the system to a consistent state despite the non-completion of the transaction. We also discuss an implementation of the modelled exception handling in the 'C' programming language as a first stage towards automatic code generation of exception handlers.

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. An alternative for capturing a modelling language’s semantics is to use the Theory plug-in to build datatypes capturing the syntactical elements of the language and operators to represent the various semantical aspects of the language. This paper draws on our experience on the statemanchines (part of SCXML) to compare the two approaches in terms of modelling efforts.

Safety and security are key considerations in the design of critical systems. Requirements analysis methods rely on the expertise and experience of human intervention to make critical judgements. While human judgement is essential to an analysis method, it is also 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. In this paper, we present a hierarchical and incremental analysis process that aims to justify the design and flow-down of derived critical requirements arising from safety hazards and security vulnerabilities identified at the system level. The safety and security analysis at each level uses STPA-style action analysis to identify hazards and vulnerabilities. At each level, we verify that the design achieves the safety or security requirements by backing the analysis with formal modelling and proof using Event-B refinement. The formal model helps to identify hazards/vulnerabilities arising from the design and how they relate to the safety accidents/security losses being considered at this level. We then re-apply the same process to each component of the design in a hierarchical manner. Thus, we use hazard and vulnerability analysis, together with refinement-based formal modelling and verification, to drive the design, replacing the system level requirements with component requirements. In doing so, we decompose critical system-level requirements down to component-level requirements, transforming them from abstract system level requirements, towards concrete solutions that we can implement correctly so that the hazards/vulnerabilities are mitigated.

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. Formal methods can address this complexity, by supporting the analysis of exception handling at the abstract design stages utilising mathematical modelling and proofs. Event-B is a state-based formal method for modelling and verifying the consistency of discrete systems. However it lacks explicit support for analysing the handling of exceptions. In this paper, we use UML-B state machines to support the modelling of normal behaviour assisting the identification and handling of exceptions. This is followed by verification of exception handler recovery mechanisms using the built-in model checker and provers of the Event-B tool-set.

In this research, we introduce the CuneiForm Abstract Characterisation method, aimed at bridging the semantic gap between textual requirements and image datasets for computer vision systems. Focusing on the case study of an Eagle Drone, we demonstrate how our CuneiForm-based approach can systematically define and validate a dataset's compliance with safety requirements. The CuneiForm characterisation process involves constructing abstract images that encapsulate objects and behaviours outlined in requirements, such as adversarial drone movements and optical appearances. These abstract images are then instantiated with actual images in training sets, ensuring a traceable link to the written specifications. Key features of our approach include meaningful mapping of real-world Target Objects of Interest (TOIs) and their environmental behaviours into pictorial models, mitigating perception failures due to TOIs' pictorial behaviours.

UML-B is a UML-like diagrammatic front end for the Event-B formal modelling language. We have been developing UML-B for over 20 years and it has gone through several iterations, each with significant changes of approach. The first version was an adaptation of a UML tool, the second generated a complete Event-B project, the third contributed parts of an Event-B model, and the fourth (currently under development) provides a human usable text persistence. Here we outline the reasons for these different developments and summarise the lessons learnt.

The increased complexity of high-consequence digital system designs with intricate interactions between numerous components has placed a greater need on ensuring that the design satisfies its intended requirements. This digital assurance can only come about through rigorous mathematical analysis of the design. This manuscript provides a detailed description of a formal language semantics that can be used for modeling and verification of systems. We use Event-B to build a formalized semantics that supports the construction of triggered enable statecharts with a run-to-completion scheduling. Rodin has previously been used to develop and analyse models using this semantics.

This paper introduces an AIC (Appreciation, Influence, and Control) based method for requirements elicitation, which describes and evaluates complex problems involving intelligent systems. Our approach integrates Critical Systems Engineering and AIC Soft Systems Design Theory for eliciting a comprehensive set of Intelligent Systems Requirements. It focuses on enhancing the architect's ability to appreciate and understand intricate intelligent behaviours in complex problems to predict emergence. Our proposed architecting strategy suggests a modelling method by transitioning from a macroscopic (holistic) view of a problem to a microscopic specification (reductionist view) of intelligent system actions in a systematic, hierarchical, incremental fashion. We consider the problem as a system of systems (soft and hard systems) to better encompass the extent of the design space and anticipate the nuances of increasing complexity after deploying an intelligent system over time. This paper bases its architecting philosophy on the AIC soft systems design theory, an incremental abstract-based system requirements derivation approach SHARCS (for hard systems design) and the HAZOP framework. The output of this process is a comprehensive set of hazardous and opportunistic scenarios and intelligent systems' behavioural requirements in those scenarios.

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. Influenced by ideas from STPA we present a hierarchical analysis process that aims to justify the design and flow-down of derived critical requirements arising from safety hazards and security vulnerabilities identified at the system level. At each level, we verify that the design achieves the safety/security requirements by backing the analysis with formal modelling and proof using Event-B refinement. The formal model helps to identify hazards/vulnerabilities arising from the design and how they relate to the safety accidents/security losses being considered at this level. We then re-apply the same process to each component of the design in a hierarchical manner. Thus we use ideas from STPA, backed by Event-B models, to drive the design, replacing the system level requirements with component requirements. In doing so, we decompose critical requirements down to components, transforming them from abstract system level requirements, towards concrete solutions that we can implement correctly so that the hazards/vulnerabilities are eliminated.

Increased systems complexity and ubiquitous computing drive the need for improved systems design. Model-based systems engineering using general purpose languages such as SysML, is a well-established response to this challenge. However, for systems where correctness-by-construction is critical, formal methods are often also deployed. This is a significant undertaking often involving complete model translation. We address this problem by developing a novel requirements interchange system, presented as a SysML model library, to guide the concurrent use of SysML and formal models without requiring complete model translation.

Constructing a large biological model is a difficult, error-prone process. Small errors in writing a part of the model cascade to the system level and their sources are difficult to trace back. In this paper we extend a recent approach based on Event-B, a state-based formal method with refinement as its central ingredient, allowing us to validate for model consistency step-by-step in an automated way. We demonstrate this approach on a model of the heat shock response in eukaryotes and its scalability on a model of the [Formula: see text] signaling pathway. All consistency properties of the model were proved automatically with computer support.

A self-driving vehicle (SDV) brings a novel idea to the automotive industry as it aims to replace the human driver; however, the human driver is still involved in the loop of an SDV's life cycle. Although the human driver plays a major role in ensuring the high-level safety property of the system, incorrect interactions between a human driver and an SDV might lead to a serious accident. Our paper aims to develop a rigorous analysis template that emphasises the system component interactions between an SDV and a human driver, especially if the SDV assumes the human driver to be a fallback option for dealing with hazardous events. Our approach combine Systems-Theoretic Processes Analysis (STPA) in order to identify the high-level safety requirements, and the Event-B formal method to provide the assurance about the consistency of the safety requirements obtained from STPA.

Biology offers many examples of large-scale, complex, concurrent systems: many processes take place in parallel, compete on resources and influence each other’s behavior. The scalable modeling of biological systems continues to be a very active field of research. In this paper we introduce a new approach based on Event-B, a state-based formal method with refinement as its central ingredient, allowing us to check for model consistency step-by-step in an automated way. Our approach based on functions leads to an elegant and concise modeling method. We demonstrate this approach by constructing what is, to our knowledge, the largest ever built Event-B model, describing the ErbB signaling pathway, a key evolutionary pathway with a significant role in development and in many types of cancer. The Event-B model for the ErbB pathway describes 1320 molecular reactions through 242 events.

A key risk with autonomous systems (AS) is the trustworthiness of the decision-making and control mechanisms that replace human control. To be trustworthy, systems need to remain safe while being resilient to unpredictable changes, functional/operational failures and cybersecurity threats. Rigorous validation and verification are essential to ensure trustworthiness of AS. Current engineering practice relies heavily on Verification and Validation (V&V) test-and-fix of system characteristics which is very time-consuming and expensive, limiting the possibilities for exploration of alternatives in system design. Instead, we focus on building a correct-by-construction system. In this paper, we present an approach to identifying and analysing mission requirements for squads of autonomous missions. Clear definition of requirements is an important pre-requisite for mission planning and for V&V of mission management. We use a structured approach to requirements identification and use formal modelling to help remove ambiguities in the requirements and to specify formal properties that should be satisfied by the missions. Our approach use a combination of analysis techniques based on Systems Theoretic Process Analysis (STPA) and formal modelling to generate critical requirements that ensure the safety and security of the system. We also suggest a compositional approach for formal modelling to enhance re-usability and address the complexity of formal modelling. Our approach is being evaluated through consideration of a combined mission of an Unmanned Surface Vehicle (USV) with deployment/recovery of small Unmanned Underwater Vehicles (UUV) within a shipping channel whereby the USV has to safely maintain station for a long period and then proceed to recover the UUV, while maintaining a communication link to an Unmanned Aerial Vehicle (UAV).

This paper presents an approach to generate SPARK code from Event-B models. System models in Event-B are translated into SPARK packages including proof annotations. Properties of the Event-B models such as axioms and invariants are also translated and embedded in the resulting models as pre- and post-conditions. This helps with generating SPARK proof annotations automatically hence ensuring the correct behaviour of the resulting code. A prototype plug-in for the Rodin has been developed and the approach is evaluated on different examples. We also discuss the possible extensions including to generate scheduled code and data structures such as records.