Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B
Ideas for a high-level proof strategy language
DEPLOY Satellite (an Attitude and Orbit Control System) Specification, Version 15
An executable "DEPLOY Satellite" specification in the form of Ada source code that has statement numbering comments. The presence of statement numbering comments is the only difference with respect to http://deploy-eprints.ecs.soton.ac.uk/166/.
School of Computing Science, Newcastle University
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.
Rodin: An Open Toolset for Modelling and Reasoning in Event-B
Workshop on B Dissemination [WOBD] Satellite event of SBMF 2010
Augmenting Formal Development of Control Systems with Quantitative Reliability Assessment
FMCO Formal Methods for Components and Objects
Proceedings of the 7th International Conference on the Quality of Information and Communications Technology
What Can the pi-calculus Tell Us About the Mondex Purse System?
Improving Testing of Enterprise Systems by Model-based Testing on Graphical User Interfaces
Software development and testing of Enterprise Resource Planning (ERP) systems demands dedicated methods to tackle its special features. As manual testing is not able to systematically test ERP systems due to the involved complexity, an efficient testing approach should be automatic. Since the underlying business processes of enterprise systems are realized at the level of the user interface (UI), system level testing is the dominant testing approach. The recent architectural shift to service-based enterprise systems demands to apply blackbox testing techniques. Model-based testing is a method that enables a high degree of automation for black-box testing, but the current research and practice usually does not address the UI. In this paper we describe the state of the art and state of the practice in order to motivate further research activities in this area.
Specification Metrics for Event-B Developments
In this paper we define several metrics for Event-B specifications in order to as-sess the maintainability of a rigorous system in its early development stage. We perform measurements of physical features of the specification. Moreover, we derive metrics like difficulty of constructing a specification or effort needed for its creation. The specification is investigated in the perspective of its syntactical characteristics. We base our metrics on the Event-B language primitives, namely operators and operands that we regard meaningful for our measurement model. We also use statistics about proof obligations in our metrics, as we consider the proving activity as a vital element in the process of creating a specification. Presented metrics are applied to a number of Event-B specifications, both their dynamic and static parts. They are examined in order to empirically con-firm appropriateness for management purposes. Obtained results are analysed in a perspective of an abstract specification and its consecutive refinements.
How to Interpret Failed Proofs in Event-B
Patterns for Modelling Time and Consistency in Business Information Systems
VSTTE’10 Verified Software: Theories, Tools and Experiments
Workshop on Tool Building in Formal Methods - ABZ Conference
Elucidating concurrent algorithms via layers of abstraction and reification
An Approach of Requirements Tracing in Formal Refinement
Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements. We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.
The Rodin platform for Event-B formal modelling is based on a bespoke model repository. While this approach has some advantages it also means that the platform does not benefit from the host of emerging technologies and supporting packages that are freely available for open source modelling frameworks. The Eclipse Modelling Framework (EMF) has emerged as the de-facto standard package upon which to build any Eclipse based modelling tool. In order to make this support available for our Rodin tools we have now engineered a front-end EMF based representation of Event-B.
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking
Abstract State Machines (ASM), Alloy, B and Z Conference (ABZ 2010)
Rewriting and Well-Definedness within a Proof System
Partiality and Recursion in Interactive Theorem Provers PAR-10
Proc. of 3rd Workshop on Model-based Testing in Practice (MOTIP'10)
A Basis for Feature-Oriented Modelling in Event-B
Feature-oriented modelling is a well-known approach for Software Product Line (SPL) development. It is a widely used method when developing groups of related software. With an SPL approach, the development of a software product is quicker, less expensive and of higher quality than a one-oﬀ development since much eﬀort is re-used. However, this approach is not common in formal methods development, which is generally high cost and time consuming, yet crucial in the development of critical systems. With the increase of more complex critical systems, it becomes more important to apply formal methods to the development cycle, and we propose a method that allows the application of SPL development techniques to formal methods. This results in faster and cheaper development of formal systems. Our method combines Event-B [1] and feature models [2]. A feature in a feature model represents a requirement of the product family and is formally described in Event-B using special feature modelling patterns. A feature repre- sented in Event-B is referred to as component. We develop composition rules, which allow components to be composed. Special composition proof obligations allow the veriﬁcation of the composition. The feature model is formed by features which may be associated with Event- B components. A subset of features from the feature model can be selected to form a feature model instance, thereby selecting several of these Event-B com- ponents. These components are composed pair-wise, and composition POs can be discharged to prove properties and to ensure consistency of the composition. The ﬁnal Event-B machine represents the formal speciﬁcation which is associated with the feature model instance and is obtained by composing these components. The motivation of our work is to allow product line development for critical systems. We use traditional product line methods, i.e. feature modelling, and link it with the formal method Event-B. Future work is focussed on amending feature diagrams to reﬂect Event-B components more precisely. Reﬁnement patterns will also be addressed.
Comparison of the AADL and Event-B Model-Based Tool Chains for Designing Embedded Systems
This paper compares two model-based tool chains support- ing the design of embedded systems. The first one relies on an architecture description language called AADL (Architecture Analysis and Design Language) specially targeting embedded system. The second one is based on a generic notation for system modelling called Event-B which is being deployed in the design of embedded systems, e.g. in the transportation sector. A number of tools supporting similar activities arehighlighted as well as the impact of the characteristics of the respective underlying languages on the global design activity.
in Proceedings of 7th Workshop on Systems Testing and Validation
Semantic Models for a Logic of Partial Functions
Verifying Mode Consistency for On-Board Satellite Software
Space satellites are examples of complex embedded systems. Dynamic behaviour of such systems is typically described in terms of operational modes that correspond to the different stages of a mission and states of the components. Components are susceptible to various faults that complicate the mode transition scheme. Yet the success of a mission depends on the correct implementation of mode changes. In this paper we propose a formal approach that ensures consistency of mode changes while developing a system architecture by refinement. The approach relies on recursive application of modelling and refinement patterns that enforce correctness while implementing the mode transition scheme. The proposed approach is exemplified by the development of an Attitude and Orbit Control System undertaken within the ICT DEPLOY project.
The Event-B method is a formal approach to modelling systems, using refinement. Initial specification is done at a high level of abstraction; detail is added in refinement steps as the development proceeds toward implementation. In previous work we developed an approach to bridge the gap between abstract specifications and implementations using an implementation level specification notation. In this paper we present details of the tool support for our notation and some of our experiences using the tool.
Tool Support for Event-B Code Generation
Eighth European Dependable Computing Conference (Fast Abstract Track)
The role of auxiliary variables in the formal development of concurrent programs
AI4FM: A New Project Seeking Challenges!
Tutorial on the modularization plugin for Event-B
This paper presents initial results of research aimed at developing methods and tools for multidisciplinary collaborative development of dependable embedded systems. We focus on the construction and analysis by co-simulation of formal models that combine discrete-event specifications of computer-based controllers with continuous-time models of the environment with which they interact. Basic concepts of collaborative modelling and co-simulation are presented. A pragmatic realisation using the VDM and Bond Graph formalisms is described and illustrated by means of an example, which includes the modelling of both normal and faulty behaviour. Consideration of a larger-scale example from the personal transportation domain suggests the forms of support needed to explore the design space of collaborative models. Based on experience so far, challenges for future research in this area are identified.
Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems
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 model which is very attractive in the industrial environment.
Event-B is a formalism for discrete system modelling. The Rodin platform provides a toolset to carry out specification, refinement and proof in Event-B. The importance of proofs as part of formal modelling cannot be emphasised enough, and as such, it is imperative to provide effective tool support for it. An important aspect of this support is the extensibility of the prover, and more pressingly, how its soundness is preserved while allowing extensibility. Rodin has a limited support for adding rules as this requires (a) a deep understanding of the internal architecture and (b) knowledge of the Java language. Our approach attempts to provide support for user-defined proof rules. We initially focus on supporting rewrite rules to enhance the rewriting capabilities of Rodin. To achieve this objective, we introduce a theory construct distinct from contexts and machines. The theory construct provides a platform for the users to define rewrite rules both conditional and unconditional. As part of rule definition, users decide whether the rule is to be applied automatically or interactively. Each defined rule gives rise to proof obligations that serve to verify its conservativity. In this respect, it is required that validity and well-definedness are preserved by rules. After the conservativity of all rules contained in a theory is established, the theory can then be deployed and available to the proving activity. In order to apply rewrite rules, it is necessary to single out applicable rules to any given sequent. This is achieved through a pattern matching mechanism which is implemented as an extension to Rodin. Our approach has two advantages. Firstly, it offers a uniform mechanism to add proof rule without the need to write Java code. Secondly, it provides a means to verify added rules using proof obligations. Our work is still in progress, and research has to be carried out to (a) cover a larger set of rewrite and inference rules, and (b) provide guidelines to help the theory developer with deciding whether a given rule should be applied automatically.
On an Extensible Rule-based Prover for Event-B
Formal Methods for Industrial Critical Systems 2010
In this paper we describe our ongoing research on Event-B specification metrics. We focus on the physical features of specification, such as its vocabulary or length for the Event-B machines. We base our metrics on the syntactic properties of the Event-B language, namely operators and operands that we consider meaningful for our measurement model. Presented metrics are applied for a number of Event-B machines. Obtained results can be analysed in a perspective of an abstract machine and its refinements.
2nd International Workshop on Software Engineering for Resilient Systems
Publication export from Deploy
This ontology contains information detailing publications held by Deploy
Formal Analysis of BPMN Models using Event-B
The use of business process models has gone far beyond documentation purposes. In the development of business applications, they can play the role of an artifact on which high level properties can be verified and design errors can be revealed in an effort to reduce overhead at later software development and diagnosis stages. This paper demonstrates how formal verification may add value to the specification, design and development of business process models in an industrial setting. The analysis of these models is achieved via an algorithmic translation from the de-facto standard business process modeling language BPMN to Event-B, a widely used formal language supported by the Rodin platform which offers a range of simulation and verification technologies.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
09381 Extended Abstracts Collection — Refinement Based Methods for the Construction of Dependable Systems
DEPLOY Satellite (an Attitude and Orbit Control System) Specification, Version 15 without statement numbering
An executable "DEPLOY Satellite" specification in the form of Ada source code without any statement numbering comment. The absence of statement numbering comments is the only difference with respect to http://deploy-eprints.ecs.soton.ac.uk/167/.
DEPLOY Work Package 3 Attitude and Orbit Control System Software Requirements Document (DEP-RP-SSF-R-005, Issue 1.0)
The 29th International Conference on Computer Safety, Reliability and Security (Safecomp 2010)
Applying Event-B Atomicity Decomposition to a Multi Media Protocol
First Workshop on Hands-on Platforms and tools for model-based engineering of Embedded Systems
Complex modern applications have to be developed to be dependable to meet their requirements and expectations of their users. An important part of this is their ability to deal with various threats (such as faults in the system environment, operator's mistakes, underlying hardware and software support problems). Development of modern applications is complicated by the need for systematic and rigorous integration of fault tolerance measures. The paper focuses on reuse of fault tolerance modelling. First, it introduces the idea of general modelling templates reflecting abstract views on system behaviour with respect to faults. These templates are used during system detalisation (re�finement) to capture the user's view on system external behaviour. Secondly, it proposes to use a library of concrete modelling patterns allowing developers to systematically integrate speci�c fault tolerance mechanisms (e.g. recovery blocks, checkpoints, exception handling) into the models. The proposed solutions are linked to the Event-B method and demonstrated using a case study.
On Fault Tolerance Reuse during Reﬁnement
International Journal on Software Tools for Technology Transfer (STTT)
Dagstuhl-Seminar 10421 "Model-Based Testing in Practice"
Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems
Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
Developing Mode-Rich Satellite Software by Refinement in Event B
To ensure dependability of on-board satellite systems, the designers should, in particular, guarantee correct implementation of the mode transition scheme, i.e., ensure that the states of the system components are consistent with the global system mode. However, there is still a lack of scalable approaches to formal verification of correctness of complex mode transitions. In this paper we present a formal development of an Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. AOCS is a complex mode-rich system, which has an intricate mode-transition scheme. We show that re�finement in Event B provides the engineers with a scalable formal technique that enables both development of mode-rich systems and proof-based verification of their mode consistency.
Model-based testing in the enterprise software domain - past and future initiatives
The testing of enterprise software poses various challenges that require a lot of effort using classical testing approaches. Model-based testing (MBT) showed its potential to improve this on several dimensions including better coverage and increased productivity both on system integration and UI-based scenario testing. In this talk we describe SAP’s recent history of MBT initiatives. A special focus is put on the identified industrial challenges, future directions inside SAP, and proposals for a global alignment of industry and academia.
Event-B Decomposition for Parallel Programs
We present here a case study developing a parallel program. The approach that we use combines reﬁnement and decomposition techniques. This involves in the ﬁrst step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via reﬁnement. Afterwards, decomposition is applied to separate the resulting model into sub-models for different processes. These sub-models are later independently developed using reﬁnement. Our approach aids the understanding of parallel programs and reduces the complexity in their proofs of correctness.
Towards Probabilistic Modelling in Event-B
System Architecture, Dependability and Modes
The mode, defining the specific type of functional behaviour that a system exhibits during its operation, is an important architectural level concept, which has a significant impact on system design, verification and dependability. The notions of modes and mode changes are widely used by the industrial engineers to structure reasoning about different conditions of system functioning. Even though there has been some work on developing modal systems, we still lack a general understanding of how to architect, verify and ensure dependability of such systems. In our work we rely on formal modelling and verification to study intricate relationships between fault tolerance, operation modes and architectural design.
Developing a Consensus Algorithm using Stepwise Refinement
We give a formal development and proof of a known consensus algorithm using stepwise refinement. We begin with an abstract specification of the intended result of the algorithm. The algorithm is developed and proved correct over a number of refinement steps. The proof of correctness is performed concurrently with the development. The development and proof make use of key fault and failure assumptions. The stepwise refinement approach allows us to introduce and prove each property at the most appropriate stage in the development, before detail irrelevant to that property has been added to the model. Finally we introduce an abstract model of a possible network on which the algorithm could be executed.
Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance
Supporting Reuse in Event B Development: Modularisation Approach
Recently, Space Systems Finland has undertaken formal Event B development of a part of on-board software for the BepiColombo space mission. As a result, lack of modularization mechanisms in Event B has been identified as a serious obstacle to scalability. One of the main benifits of modularization is that it allows us to decompose system models into components that can be independently developed. It also helps to manage complexity of models that in the industrial setting are usually very large and difficult to comprehend. On the other hand, modularization enables reuse of formally developed components in the formal product line development. In this paper we propose a conservative extension of Event B formalism to support modularization. We demonstrate how our approach can support reuse in the formal development in the space domain.
15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010)
Model-driven Service Integration Testing - A Case Study
This paper presents a case study for the modeling and model-based testing (MBT) of enterprise service choreographies. Our proposed MBT approach uses poprietary models called Message Choreography Models (MCM) as test models. The case study illustrates how MCM-based service integration testing allows to formalize design decisions and enables full integration into an existing industrial test infrastructure by using the concepts of domain specific languages and model transformations. Further, the MBT tools integrated into the testing framework have been compared based on one concrete use case.
Mathematical Extension in Event-B through the Rodin Theory Component