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.

As the physical world evolves with time, safety-critical systems are usually used with time-dependent functionality. The design and implementation of real-time systems are challenging due to the complicated functional and timing requirements. Event - B formalization offers a stepwise development approach for specifying and verifying systems with mathematical techniques and tools. In this paper, we propose four realtime specification patterns, namely time response pattern, abort pattern, intermediate pattern and periodic pattern, to facilitate the specification of real-time properties in Event-B models. The proposed patterns are used in a dual-chamber pacemaker case study to specify and verify the timing cycles based on the requirements. The model is proved using the Rodin tool.

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.

Abstraction and refinement offer a stepwise development approach to managing complexity in system design. Based on our previous work that extends Event-B models with high level real-time trigger-response properties, this paper presents refinement semantics of timed systems using behavioral traces. Forward simulation, which is a proof technique for refinement, is used to verify the consistency between different refinement levels. To prove refinement of trace semantics, we construct intermediate traces from concrete traces with a mapping function and prove the intermediate trace without stuttering events and states are abstract traces. Fairness assumptions, relative deadlock freedom, and conditional convergence are adopted in refinement steps to eliminate Zeno behavior in timed models. Based on the semantics, we develop refinement rules and strategies to perform refinement on timed models and refine real-time trigger-response properties into sequential or alternative sub-timing properties with proofs.

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 is a formal method for system-level modelling and analysis, which uses logic and set theory to describe discrete labelled transition systems. Timed transition systems have been introduced to incorporate timing constraints on transitions to describe real-time behaviours of the system. This paper proposes an approach to modelling high level timing constraints between different transitions with a timed trigger-response property. We present trace semantics for the trigger-response property and timed trigger-response property. This semantics provides a precise definition of valid trigger-response behaviours in Event-B machines. Based on the semantics, we develop proof obligations on Event-B machines under which all the traces of a machine satisfy the trigger-response property and the timed trigger-response property.

Event-B is a state-based formal method for modelling and verifying the consistency of discrete systems. Event refinement structures (ERS) augment Event-B with hierarchical diagrams, providing explicit support for workflows and refinement relationships. Despite the variety of ERS combinators, ERS still lacks the flexibility to model dynamic workflows that support dynamic changes in the degree of concurrency. Specifically in the cases where the degree of parallelism is data dependent and data values can change during execution. In this paper, we propose two types of extensions in ERS to support dynamic modelling using Event-B. The first extension is supporting data-dependent workflows where data changes are possible. The second extension improves ERS by providing exception handling support. Semantics are given to an ERS diagram by generating an Event-B model from it. We demonstrate the Event-B encodings of the proposed ERS extensions by modelling a concurrent emergency dispatch case study.

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.

No abstract available.

No abstract available.

No abstract available.

Abstract Event-B is a formal method for modelling and verifying the consistency of chains of model refinements. The event refinement structure (ERS) approach augments Event-B with a graphical notation which is capable of explicit representation of control flows and refinement relationships. In previous work, the ERS approach has been evaluated manually in the development of two large case studies, a multimedia protocol and a spacecraft sub-system. The evaluation results helped us to extend the ERS constructors, to develop a systematic definition of ERS, and to develop a tool supporting ERS. We propose the ERS language which systematically defines the semantics of the ERS graphical notation including the constructors. The ERS tool supports automatic construction of the Event-B models in terms of control flows and refinement relationships. In this paper we outline the systematic definition of ERS including the presentation of constructors, the tool that supports it and evaluate the contribution that ERS and its tool make. Also we present how the systematic definition of ERS and the corresponding tool can ensure a consistent encoding of the ERS diagrams in the Event-B models.

The Simulink/Stateflow (SL/SF) modeling framework is widely used in industry for the development of control applications. However, such models are not amenable to formal reasoning. Controllers can also be designed using formal specification languages. Such designs can be formally verified, but the models do not explicitly represent control or data flow information. In this paper, we discuss RRM diagrams (RRMDs), a new modelling notation which incorporates the benefits of these two formalisms. RRMDs are graphical formal models and they also support incremental formal development. We have used synchronising state machines to encode RRMDs. We have also developed a prototype tool which translates RRMDs automatically to SL/SF designs.

No abstract available.

Abstract Abrial’s Event-B formalism for refinement-based system development is influenced by Back’s action system approach. Morgan has defined a CSP-like failures-divergence semantics for action systems that distinguishes internal and external choice of actions. Morgan’s semantics has the characteristic that the choice between enabled actions is external while internal choice is represented less directly through nondeterministic effect of actions. Practical experience with Event-B has demonstrated the need to be able to represent both internal and external choice between enabled events more explicitly. In this paper, Morgan’s failures semantics for action systems is modified to allow both internal and external choice to be represented directly. This is achieved by grouping events so that external choice is between event groups and internal choice is within event groups. This leads to a refinement rule for preservation of choice between event groups while allowing for reduction of choice within event groups. We also provide a refinement rule for splitting event groups in order to increase external choice. The refinement rules are justified in terms of failures refinement.

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.

No abstract available.

Abstract A development of the Mondex system was undertaken using Event-B and its associated proof tools. An incremental approach was used whereby the refinement between the abstract specification of the system and its detailed design was verified through a series of refinements. The consequence of this incremental approach was that we achieved a very high degree of automatic proof. The essential features of our development are outlined. We also present some modelling and proof guidelines that we found helped us gain a deep understanding of the system and achieve the high degree of automatic proof.

Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric states. This paper presents a framework for symmetry reduced model checking of B machines, which verifies a unique representative from each orbit. Symmetries are induced by the deferred set; a key component of the B language. This contrasts with strategies that require the introduction of a special data type into a language, to indicate symmetry. An extended version of the graph isomorphism program, nauty, is used to detect symmetries, and the symmetry reduction package has been integrated into the PROB model checker. Relevant algorithms are presented, and experimental results illustrate the effectiveness of the method, where exponential speedups are sometimes possible.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

No abstract available.

The emergence of the UML as a de facto standard for object-oriented modeling has been mirrored by the success of the B method as a practically useful formal modeling technique. The two notations have much to offer each other. The UML provides an accessible visualization of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilize a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specializations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioral modeling. The design of UML-B has been guided by industrial applications.

Abstract. Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification A to a concrete specification C that is as least as deterministic. Knowing A and C one proves that C refines, or implements, specification A . In this study we consider specification A as given and concern ourselves with a way to find a good candidate for implementation C . To this end we classify all implementations of an abstract specification according to their performance. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification correctly are excluded. Only the remaining correct implementations C are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary for the performance of any implementation. We introduce the probabilistic action system formalism which combines refinement with performance. In our current study we measure performance in terms of long-run expected average-cost. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. A corresponding notion of refinement and simulation-based proof rules are introduced. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification A thus assisting in the search for a good implementation C .

The UML (Unified Modeling Language) state diagram notation by M. Fowler and K. Scott (2000) is a graphical language which comprises an extensive set of constructs with good structural semantics but lack of a formal behavioral semantics. With this regard, we have used the Hoare's CSP (Communicating and Sequential Processes) to formalize the behavior of UML SD. The fact that CSP is supported by model-checkers such as FDR enables a system design using a state diagram to be formally checked during design stage. This paper presents the formalization which would allow us to reason about the behavior of UML SD in CSP.

Abstract. We report on experiences gained from the application of data refinement techniques to the development of examples of secure communications systems. The aim was to the carry the development from initial abstract specification of security services through to detailed designs. The development approach was based on action systems, with B and CSP being used as concrete notations. The security services in question are a confidential communications service and an authenticated transaction service. Refinements include explicit representations of intruder behaviour. The paper makes several interrelated contributions. It demonstrates the feasibility of applying a refinement approach to this type of problem, including an effective way of combining B and CSP in refinements. It introduces a more systematic approach to the development of abstraction invariants and refinement checking. Finally, it illustrates the limitation, when modelling security protocols, of a formalism that does not deal with probability.

Abstract. This paper describes the tool csp2B, which provides a means of combining CSP-like descriptions with standard B specifications. The notation of CSP provides a convenient way of describing the order in which the operations of a B machine may occur. The function of the tool is to convert CSP-like specifications into standard machine-readable B specifications, which means that they may be animated and appropriate proof obligations may be generated. Use of csp2B means that abstract specifications and refinements may be specified purely using CSP or using a combination of CSP and B. The translation is justified in terms of an operational semantics.

Grover's search algorithm is designed to be executed on a quantum-mechanical computer. In this article, the probabilistic wp -calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus provides a rigorous programming notation for modeling this and other quantum algorithms and that it also provides a systematic framework of analyzing such algorithms.

Abstract Morgan [Mor90a] has described a correspondence between Back's action systems [BKS83] and the conventional failures-divergences model of Hoare's communicating sequential processes (CSP) formalism [Hoa85]. However, the CSP failures-divergences model does not treat unbounded nondeterminism, although unbounded nondeterminism arises quite naturally in action systems; to that extent, the correspondence between the two approaches is inadequate. Fortunately there is an extended infinite traces model of CSP [RoB89] which treats unbounded nondeterminism. We extend the CSP-action system correspondence, using that model instead, to take the unbounded nondeterminism of action systems properly into account. In passing, we develop a definition of the weakest precondition under which an infinite heterogeneous trace of actions is enabled.