This paper presents a methodology called Rigorous Analysis Template Process (RATP) for analysing the behaviours and interactions of multiple components in a Self-Driving Vehicle (SDV) to ensure its system safety, especially when a human driver is involved as a fallback option for handling hazardous events. RATP uses Systems-Theoretic Processes Analysis (STPA) and Event-B formal method to gradually identify safety requirements and build their rigours models. The output of RATP is a set of safety requirements that guide the development of a rigorous model to maintain the system safety against identified hazardous states at different levels of abstraction. The main advantage of RATP is to allow the behaviours of a system to be analysed from a high-abstraction layer to a more detailed concrete layer.

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.

Stepwise development supported by the Event-B formalism has been used in the domain of system design and verification. This refinement approach guarantees that safety properties are preserved, while additional reasoning is required to prove the preservation of liveness properties. Our previous work proposes to use real-time trigger-response properties to reason about liveness properties and timed properties in real-time systems. Conditions such as weak fairness assumptions, relative deadlock freedom, and conditional convergence are explored to eliminate Zeno behavior when modeling real-time systems. In this reasoning framework, some strong constraints do not apply to real-world cases. This paper extends our previous results by using strong fairness assumptions to relax these constraints. We present the proof obligations together with temporal properties to construct the theorems and proofs. Fairness assumptions are used to enforce real-time properties in Event-B models. The carrier-sense multiple access with collision detection protocol is used as a case study to illustrate the approach.

Behaviour driven formal model development (BDFMD) enables domain engineers to influence and validate mathematically precise and verified specifications. In previous work we proposed a process where manually authored scenarios are used initially to support the requirements and help the modeller. The same scenarios are used to verify behavioural properties of the model. The model is then mutated to automatically generate scenarios that have a more complete coverage than the manual ones. These automatically generated scenarios are used to animate the model in a final acceptance stage. In this paper, we discuss lessons learned from applying this BDFMD process to a real-life specification: The European Train Control Systems (ETCS) Hybrid Level 3. During the case study, we have developed our understanding of the process, modifying the way we do some stages and developing improved tool support to make the process more efficient. We discuss (1) the need for abstract scenarios during incremental model development and verification, (2) tools and techniques developed to make the running of scenarios more efficient, and (3) improvements to tools that generate new test cases to improve coverage.

Formal modelling methods rightly focus on the primary goal of verifying properties. This can however, lead to inadequate facilities for structuring the model into manageable verification components. For example, the Event-B language is designed to achieve a high level of automatic theorem proofs through a linear sequence of refinements. In previous work, we introduced a mechanism to structure models via an inclusion mechanism using event synchronisations but this did not deal with generalised instantiations of a model component. Here we introduce a lifting mechanism that can be used in conjunction with inclusion to introduce multiple instances of a separately verified model lifted to an arbitrary set of instances. This allows localised properties to be proven without the complications caused by multiple instances as well as enhancing the usability of the inclusion feature.

Event-B developments are mostly structured around the refinement relationship. This top-down development architecture enables system details to be gradually introduced into the formal model. However, this results in large models with monolithic structures. We develop a composition mechanism allowing to develop models bottom-up. In particular, our proposed mechanism works seamlessly with the existing refinement technique in Event-B. As a result we have built a formal development method that can take advantage of both top-down and bottom-up approaches. We prove the correctness of machine inclusion with refinement using the supporting Rodin platform.

We present an approach for ensuring safety properties of autonomous systems. Our contribution is a system architecture where a policing function validating system safety properties at runtime is separated from the system's intelligent planning function. The policing function is developed formally by a correct-by-construction method. The separation of concerns enables the possibility of replacing and adapting the intelligent planning function without changing the validation approach. We validate our approach on the example of a multi-UAV system managing route generation. Our prototype runtime validator has been integrated and evaluated with an industrial UAV synthetic environment.

Abstract In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.

Mobile distributed systems involve specific aspects such as migration, communication and concurrency, usually under temporal constraints. In this paper, we deal with formal modelling of timed migrating and communicating processes, as provided by the TiMo calculus. In this framework, mobile processes can move between different locations and communicate when collocated, all this happening in the presence of local timers. Our contribution is a general framework for reasoning about systems specified using TiMo. We use the Event-B modelling method as the target for translating TiMo specifications. Subsequently, we utilise the supporting Rodin platform of Event-B to verify system properties using the embedded theorem-provers and model checkers. The main feature of our encoding include a generic model capturing the syntax and semantics of TiMo, together with a concrete model corresponding to each specific TiMo specification. We illustrate our approach by a non-trivial example featuring different concepts of TiMo.

Abstract The Shadow Semantics (Morgan, Math Prog Construction, vol 4014, pp 359–378, 2006 ; Morgan, Sci Comput Program 74(8):629–653, 2009 ) is a possibilistic (qualitative) model for noninterference security. Subsequent work (McIver et al., Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, 2010 ) presents a similar but more general quantitative model that treats probabilistic information flow. Whilst the latter provides a framework to reason about quantitative security risks, that extra detail entails a significant overhead in the verification effort needed to achieve it. Our first contribution in this paper is to study the relationship between those two models (qualitative and quantitative) in order to understand when qualitative Shadow proofs can be “promoted” to quantitative versions, i.e. in a probabilistic context. In particular we identify a subset of the Shadow’s refinement theorems that, when interpreted in the quantitative model, still remain valid even in a context where a passive adversary may perform probabilistic analysis. To illustrate our technique we show how a semantic analysis together with a syntactic restriction on the protocol description, can be used so that purely qualitative reasoning can nevertheless verify probabilistic refinements for an important class of security protocols. We demonstrate the semantic analysis by implementing the Shadow semantics in Rodin, using its special-purpose refinement provers to generate (and discharge) the required proof obligations (Abrial et al., STTT 12(6):447–466, 2010 ). We apply the technique to some small examples based on secure multi-party computations.

Abstract The Shadow semantics is a qualitative model for noninterference security for sequential programs. In this paper, we first extend the Shadow semantics to Event-B, to reason about discrete transition systems with noninterference security properties. In particular, we investigate how these security properties can be specified and proved as machine invariants. Next we highlight the role of security invariants during refinement and identify some common patterns in specifying them. Finally, we propose a practical extension to the supportingRodin platformof Event-B, with the possibility of having some properties to beinvariants-by-construction.

Abstract Two methods have been identified for Event‐B model decomposition: shared variable and shared event. The purpose of this paper is to introduce the two approaches and the respective tool support in the Rodin platform. Besides alleviating the complexity for large systems and respective proofs, decomposition allows team development in parallel over the same Event‐B project which is very attractive in the industrial environment. Copyright © 2011 John Wiley & Sons, Ltd.

Event-B has given developers the opportunity to construct models of complex systems which are correct by construction. However, there is no systematic approach, especially in terms of reusing, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the future tool support within the associated Rodin Platform of Event-B. The approach has been applied successfully in some medium-size industrial case studies.

Abstract The introduction of probabilistic behaviour into the B-method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected values of the machine state can be expressed and verified. This paper explores the application of probabilistic B to a simple case study: tracking the volume of liquid held in a tank by measuring the flow of liquid into it. The flow can change as time progresses, and sensors are used to measure the flow with some degree of accuracy and reliability, modelled as non-deterministic and probabilistic behaviour respectively. At the specification level, the analysis is concerned with the expectation clause in the probabilistic B machine and its consistency with machine operations. At the refinement level, refinement and equivalence laws on probabilistic GSL are used to establish that a particular design of sensors delivers the required level of reliability.