Search

Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods. Open image in new window , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage Open image in new window tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Open image in new window refinements and suggest a solution. We outline how safety and liveness properties could be verified.

We present the CamilleX framework for the Rodin platform in this paper. The framework provides a textual representation and persistence for the Event-B modelling constructs. It supports direct extensions to the Event-B syntax such as machine inclusion and record structures, as well as indirect extensions provided by other plugins such as UML-B diagrams. We discusses CamilleX’s design and in particular, its extension mechanisms and examples of their use.

Event-B, a refinement-based formal modelling language, has traditionally focused on safety, but now increasingly finds a new role in developing secure systems. In this paper we take a fresh look at security and focus on what security means for the system rather than looking at detailed protocols. We use Event-B for proving security from an abstract view and refining it towards design details, focusing on the refinement of the availability property of the system. We define a general approach to guarantee the availability of events by ensuring the non-strengthening of their guards, taking into consideration their parameter types.We illustrate our approach using a smart ballot system, an integral part of modern voting systems.

Formal methods use abstraction and rigorously verified refinement to manage the design of complex systems, ensuring that they satisfy important invariant properties. However, formal verification is not sufficient: models must also be tested to ensure that they behave according to the informal requirements and validated by domain experts who may not be expert in formal modelling. This can be satisfied by scenarios that complement the requirements specification. The model can be animated to check whether the scenario is feasible in the model and that the model reaches the states expected in the scenario. However, there are two problems with this approach. 1) The natural language used to describe the scenarios is often verbose, ambiguous and therefore difficult to understand; especially if the modeller is not a domain expert. 2) Provided scenarios are typically at the most concrete level corresponding to the full requirements and cannot be used until all the refinements have been completed in the model. We show by example how a precise and concise domain specific language can be used for writing these abstract scenarios in a style that can be easily understood by the domain expert (for validation purposes) as well as the modeller (for behavioural verification) and can be used as the persistence for automated tool support. We propose two alternative approaches to using scenarios during formal modelling: A method of refining scenarios before the model is refined so that the scenarios guide the modelling, and a method of abstracting scenarios from provided concrete ones so that they can be used to test early refinements of the model. We illustrate the two approaches on the ‘Tokeneer’ secure enclave example and the ERTMS/ETCS Hybrid Level 3 specification for railway controls. We base our approach on the Cucumber framework for scenarios and the Event-B modelling language and tool set. We have developed a new ‘Scenario Checker’ plugin to manage the animation of scenarios. 1

State-based formal specifications benefit from data structuring mechanisms, which collate associated properties and efficiently declare complex types. For example, ‘record’ data structures, similar to those used in programming languages, can be built into the concrete syntax of a language as an enhancement over flat data relationships. While this is relatively simple to achieve for a single-level specification, it becomes significantly more involved when the specification language allows for progressive refinement of the data supporting the specification. Individual fields may be added to create sub-records within a refinement and replaced to create refined records during a refinement step. The impact on the ability to verify invariant and refinement proof obligations must be considered. Here we describe a record structuring syntax that includes notions of extension and inheritance that can be used in a refinement-based formal method. We illustrate the approach using extensions to the Event-B formal method.

Event-B is a state-based formal method for system development. The Event-B mathematical language does not support a syntax for the direct definition of structured types such as records. This paper proposes extending the Event-B language with direct record definitions. A key feature is the ability to extend records with new fields in refinement steps. The XEvent-B tool, which supports a textual representation of Event-B models, is extended to provide support for direct record definition and automatic transformation of record structures into standard Event-B elements. We demonstrate this work by modelling of the Tokeneer case study.

The Theory plug-in for the Rodin Platform enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support for reasoning about the extended language. We consider in this chapter using Rodin theories to capture domain-specific Abstract Data Types (ADTs) and build dynamic systems using the developed structures. In particular, we propose the notion of theory instantiation to incorporate more concrete representation of the ADTs. At the same time, the dynamic systems are refined further with respect to the changes of the underlying ADTs. We illustrate our approach with an industrial example of developing a CBTC train control system. We anticipate theory instantiation to be a promising direction for reusing theories via abstraction.

Although popular in industry, state-chart notations with ‘run to completion’ semantics lack formal refinement and rigorous verification methods. State-chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage Event-B ’s tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how critical (e.g. safety) invariant properties can be verified by proof despite the reactive nature of the system. We also show how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic model checking approach.

Cross-layer runtime management (RTM) frameworks for embedded systems provide a set of standard APIs for communication between different system layers (i.e. RTM, applications and device) and simplify the development process by abstracting these layers. Integration of independently developed components of the system is an error-prone process that requires careful verification. In this paper, we propose a formal approach to integration testing through automatic generation of runtime assertions in order to test the implementation of the APIs. Our approach involves a formal model of the APIs, developed using the Event-B formal method which is automatically translated to a set of assertions and embedded in the existing implementation of APIs. The embedded assertions are used at runtime to check the correctness of the integration. This work was supported by the EPSRC PRiME Project (EP/K034448/1), www.prime-project.org.

This chapter presents the results of the railway domain. It focuses on the validation of a route control system using a model-based approach and formal methods. A main technical challenge is the automation of the translation step between a formalized specification and a mathematical model which allows for proofs of functional and safety properties of the solution.

The increased connectivity of critical maritime infrastructure (CMI) systems to digital networks have raised concerns of their vulnerability to cyber attacks. As less emphasis has been placed, to-date, on ensuring security of cyber-physical maritime systems, mitigating these cyber attacks will require the design and engineering of secure maritime infrastructure systems. Systems theory has been shown to provide the foundation for a disciplined approach to engineering secure cyber-physical systems. In this paper, we use systems theory, and concepts adapted from safety analysis, to develop a systematic mechanism for analysing the security functionalities of assets’ interactions in the maritime domain. We use the theory to guide us to discern the system’s requirement, likely system losses, potential threats, and to construct system constraints needed to inhibit or mitigate these threats. Our analyses can be used as springboards to a set of principles to help enunciate the assumptions and system-level security requirements useful as the bases for systems’ security validation and verification.

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 methods use abstraction and rigorously verified refinement to manage the design of complex systems, ensuring that they satisfy important invariant properties. However, formal verification is not sufficient: models must also be tested to ensure that they behave according to the informal requirements and validated by domain experts who may not be expert in formal modelling. This can be satisfied by scenarios that complement the requirements specification. The model can be animated to check that the scenario is feasible in the model and that the model reaches states expected in the scenario. However, there are two problems with this approach. (1) The provided scenarios are at the most concrete level corresponding to the full requirements and cannot be used until all the refinements have been completed in the model. (2) The natural language used to describe the scenarios is often verbose, ambiguous and therefore difficult to understand; especially if the modeller is not a domain expert. In this paper we propose a method of abstracting scenarios from concrete ones so that they can be used to test early refinements of the model. We also show by example how a precise and concise domain specific language can be used for writing these abstract scenarios in a style that can be easily understood by the domain expert (for validation purposes) as well as the modeller (for behavioural verification). We base our approach on the Cucumber framework for scenarios and the Event-B modelling language and tool set. We illustrate the proposed methods on the ERTMS/ETCS Hybrid Level 3 specification for railway controls (The example model and scenario scripts supporting this paper are openly available at https://doi.org/10.5258/SOTON/D1026).

Statechart modelling notations, with so-called ‘run to completion’ semantics and simulation tools for validation, are popular with engineers for designing systems. However, they do not support formal refinement and they lack formal static verification methods and tools. For example, properties concerning the synchronisation between different parts of a system may be difficult to verify for all scenarios, and impossible to verify at an abstract level before the full details of sub-states have been added. Open image in new window , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible, restricting instantiation and testing to a validation role. In this paper, we introduce a notion of refinement, similar to that of Open image in new window , into a ‘run to completion’ Statechart modelling notation, and leverage Open image in new window ’s tool support for proof. We describe the pitfalls in translating ‘run to completion’ models into Open image in new window refinements and suggest a solution. We illustrate the approach using our prototype translation tools and show by example, how a synchronisation property between parallel Statecharts can be automatically proven at an intermediate refinement level.

Correct operation of many critical systems is dependent on the data consistency and integrity properties of underlying databases. Therefore, a verifiable and rigorous database design process is highly desirable. This research aims to investigate and deliver a comprehensive and practical approach for modelling databases in formal methods through layered refinements. The methodology is being guided by a number of case studies, using abstraction and refinement in UML-B and verification with the Rodin tool. UML-B is a graphical representation of the Event-B formalism and the Rodin tool supports verification for Event-B and UML-B. Our method guides developers to model relational databases in UML-B through layered refinement and to specify the necessary constraints and operations on the database., In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636

This paper proposes a new extension to the Event-B modelling method to facilitate the building of hierarchical mathematical libraries to ease the formal modelling of many systems. The challenges are to facilitate building mathematical theories, be compatible with the current method and tools, and to be extensible by users within the Rodin Platform supporting Event-B.Our contribution is a new language, called B#, which includes the additional features of type classes and sub-typing. The B# language compiles to the current language used by the Rodin's Theory Plug-in, which ensures consistency, and also gives compatibility with the current Rodin tools. We demonstrate the advantages of the new language by comparative examples with the existing Theory Plug-in language.

Scheduled Event-B (SEB) augments Event-B with a scheduling language to make the control flow in an Event-B model explicit and facilitate derivation of algorithmic structure in Event-B refinement. A concrete SEB model has a concrete algorithmic structure associated with it. Although this structure reduces the difficulty of code generation, there is still some gap between the model and executable code. This work formulates the translation of SEB models to a programming language called Dafny and proposes an approach in which a number of assertions are generated from the model that allows the verification of the generated code in a static program verifier.

We present a formal specification and analysis of a haemodialysis machine (HD machine) in Event-B using the Rodin Toolset. The medical device domain is a particularly complex multidisciplinary field involving disparate branches of engineering, biological and medical fields as well as a critical patient-machine interface. Requirements include safety properties, process steps, human–machine interfaces, timing constraints, dynamic control algorithms, and design features. Our aim is to demonstrate that the Event-B based modelling, verification and validation tools deal with the variety of requirements involved in a typical medical device. We utilise ProR for structuring and tracking requirements. We model the HD machine using iUML-B state-machines and class diagrams, and build a corresponding BMotion Studio visualisation. For verification, we use both theorem proving and model checking techniques. We validate the design of the system using (i) diagrams to aid the modelling of the sequential properties of the requirements, and (ii) ProB-based animation and visualisation tools to explore the system's behaviour. Some of the safety properties involve dynamic behaviour which is difficult to verify in Event-B. For these properties we use (iii) co-simulation tools to validate against a continuous model of the physical behaviour. We conclude that the Event-B based modelling tools are particularly rich in verification and validation techniques and with the help of supporting tools for requirements tracking, are able to address the different kinds of requirements in a medical device.

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.

Cyber-physical systems represent an engineering challenge due to their safety and security concerns, particularly those systems involved in critical infrastructure which require some of the highest standards of safety, availability, integrity and security. The complexity of these systems makes the identification and analysis of safety and security requirements challenging. In this paper, we present a methodology for identifying and formally analysing safety and security requirements, based on the STPA methodology and combined with modelling, traceability and formal verification through use of the Event-B formal method. Our STPA approach is then leveraged to generate ‘critical requirements’ to mitigate against undesirable system states, which are subsequently translatedinto constraints on an Event-B representation of the system. The Rodin toolset allows us to demonstrate that these critical requirements fully mitigate against the undesirable system states and therefore provide automated verification of the critical requirements.

Automatic recognition of behaviours and events from visual data is an emerging topic in video surveillance. These methods promise the ability to derive contextual awareness for a scene and may further enable the ability to predict the intentions of the subject. This paper describes a novel system for analysing human behaviours in the context of a video surveillance application. This may be used to distinguish between normal and anomalous behaviours. We propose a novel framework for the application of behaviour recognition and summarisation using interval type-2 fuzzy logic classification systems (IT2FLS). We employ the evolutionary-based technique Big Bang Big Crunch (BB-BC) to automatically optimise parameters of membership functions (MFs) and rules in the IT2FLSs. Our analysis shows that the BB-BC IT2FLS is able to robustly recognise behaviours and furthermore outperforms both its' conventional IT2FLS (which does not employ fuzzy classification techniques) and Type-1 FLSs (T1FLSs) counterparts in addition to non-fuzzy recognition methods.

Originally designed to be used as dedicated coprocessors, GPUs have progressively become part of shared computing environments, such as HPC servers and clusters. Commonly used GPU software stacks (e.g., CUDA and OpenCL), however, are designed for the dedicated use of GPUs by a single application, possibly leading to resource underutilization when multiple applications share the GPU resources. In recent years, several node-level runtime components have been proposed to target this problem and allow the efficient sharing of GPUs among concurrent applications. The concurrency enabled by these systems, however, is limited by synchronizations embedded in the applications or implicitly introduced by the GPU software stack. This work targets this problem. We first analyze the effect of explicit and implicit synchronizations on application concurrency and GPU utilization. We then design runtime mechanisms to bypass these synchronizations, along with a memory management scheme that can be integrated with these synchronization avoidance mechanisms to improve GPU utilization and system throughput. We integrate these mechanisms into a recently proposed GPU virtualization runtime named Sync-Free GPU (SF-GPU), thus removing unnecessary blockages caused by multitenancy, ensuring any two applications running on the same device experience limited to no interference, maximizing the level of concurrency supported. We also release our mechanisms in the form of a software API that can be used by programmers to improve the performance of their applications without modifying their code. Finally, we evaluate the impact of our proposed mechanisms on applications run in isolation and concurrently.

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B., In Proceedings PAR 2010, arXiv:1012.4555

We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a refinement checker, both of which can be used to detect various errors in B specifications. We describe the underlying methodology of ProB, and present the important aspects of the implementation. We also present empirical evaluations as well as several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.

Run-Time Management (RTM) systems are used to control energy hooks at run-time to minimise the energy consumption of embedded systems with single and many-core processors. Typically, such RTM systems are aware of application requirements and utilise workload prediction and machine learning algorithms to estimate the optimal configuration. An RTM mechanism should not compromise the reliability or performance of the platform it is managing. Because of the potential complexity and interaction with the platform and its applications, we are using rigorous design methods that allow us to master the complexity and verify the correctness of our designs in a formal way. The formal RTM design can be verified earlier in the development process before implementation, which early verification can reduce the cost of fixing potential failures which can be very demanding in testing the system after implementation. In addition, the formal model of a RTM system can be automatically translated into executable code to be executed on the hardware. Automatic code generation reduces the efforts of hand-coded implementation and is portable across different architectures and Operating Systems (OSs). In this paper we propose a formal approach toward automatic generation of RTM system code, for a video decoder application, from a verified formal model of a RTM. The formal model of the RTM system is developed using the Event-B formal modelling language and is verified using theorem proving and model checking. The automatically generated RTM system has been integrated in an embedded platform as a Linux governor, and provides up to 4% improvement over Linux's default Ondemand governor.

The constructive approach to software correctness aims at formal modelling and verification of the structure and behaviour of a system in different levels of abstraction. In contrast, the analytical approach to software verification focuses on code level correctness and its verification. Therefore it would seem that the constructive and analytical approaches should complement each other well. To demonstrate this idea we present a case for linking two existing verification methods, Event-B (constructive) and Dafny (analytical). This approach combines the power of Event-B abstraction and its stepwise refinement with the verification capabilities of Dafny. We presented a small case study to demonstrate this approach and outline of the rules for transforming Event-B events to Dafny contracts. Finally, a tool for automatic generation of Dafny contracts from Event-B formal models is presented.

We describe a formal approach to the development of embedded controllers for a railway. The approach starts with a system-level specification modeling the system under control and the desired control behavior. Correctness-preserving refinement is then used to add more and more implementation detail to the models and to decompose the models into sub-systems to arrive at models of individual controllers. The B Method is used as the formal notation and methodology.

A Run-Time Management system for many-core architecture is aware of application requirements and able to save energy by sacrificing performance when it will have negligible impact on user experience. This paper outlines the application of a process for development of a run-time management system that integrates a range of modelling, validation, verification and generation tools at appropriate stages. We outline the models, process and tools we used to develop a temperature aware run-time management system for Dynamic Voltage and Frequency Scaling (DVFS) of a media display application. The Event Refinement Structure (ERS) approach is used to visualise the abstract level of the DVFS control. The Model Decomposition technique is used to tackle the complexity of the model. To model the process-oriented aspects of the system we used iUML-B Statemachines. We use several different visual animation tools, running them synchronously to exploit their different strengths, in order to demonstrate the model to stakeholders. In addition, a continuous model of the physical properties of the cores is simulated in conjunction with discrete simulation of the Event-B run-time management system. Finally executable code is generated automatically using the Code Generation plug-in. The main contribution of this paper is to demonstrate the complementarity of the tools and the ease of their integrated use through the Rodin platform.

Constructing traceable Event-B models from requirements is crucial in the system development process. It enables the validation of the model against the requirements and allows to identify different refinement levels, which is a key to successful formal modelling with a refinement-based method. Our objective is to present an approach based on the use of semi-formal structures to bridge the gap between requirements and Event-B models and retain traceability to requirements in Event-B models. The presented approach makes use of the UML-B and Atom- icity Decomposition (AD) approaches. UML-B provides UML graphical notation that enables the development of an Event-B formal model, while the AD approach provides a graphical notation to illustrate the refinement structures and assists in the organisation of refinement levels. The AD approach also combines several con- structor patterns to manage control flows in Event-B. The intent of this paper is to harness the benefits of the UML-B and AD approaches to facilitate constructing Event-B models from requirements and provide traceability between requirements and Event-B models., Electronic Communications of the EASST, Volume 66: Automated Verification of Critical Systems 2013

This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component behaviour is specified through a combination of UML-B state machines and Event-B. CODA communications and timing are given an Event-B semantics through translation rules. Refinement is based on Event-B refinement and allows layered construction of CODA models in a consistent way., Comment: In Proceedings Refine 2013, arXiv:1305.5634

UML-B is a ‘UML-like’ graphical front end for Event-B that provides support for object-oriented and state-machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state-machine diagram editors with automatic generation of corresponding Event-B. In Event- B, refinement is used to relate system models at different abstraction levels. The same refinement concepts are also applicable in UML-B but require special consideration due to the higher-level modelling concepts. In previous work we described a case study to introduce support for refinement in UML-B. We now provide a more complete presentation of the technique of refinement in UML-B including a formalisation of the refinement rules and a definition of the extensions to the abstract syntax of UML-B notation. The provision of gluing invariants to discharge the proof obligations associated with a refinement is a significant step in providing verifiable models. We discuss and compare two approaches for constructing gluing invariants in the context of UML-B refinement.

The action system formalism [6] is a state-based approach to distributed computing. In this paper, it is shown how the action system formalism may be used to describe systems that communicate with their environment through synchronised value-passing. Definitions and rules are presented for refining and decomposing such action systems into distributed implementations in which internal communication is also based on synchronised value-passing. An important feature of the composition rule is that parallel components of a distributed system may be refined independently of the rest of the system. Specification and refinement is similar to the refinement calculus approach [4, 26, 28]. The theoretical basis for communication and distribution is Hoare's CSP [16]. Use of the refinement and decomposition rules is illustrated by the design of an unordered buffer, and then of a distributed message-passing system.

The Event-B method is a formal modelling approach; our interest is the final step, of generating code for concurrent programs, from Event-B. Our Tasking Event-B tool integrates Event-B to facilitate code generation. The theory plug-in allows mathematical extensions to be added to an Event-B development. When working at the implementation level we need to consider how to translate the newly added types and operators into code. In this paper, we augment the theory plug-in, by adding a Translation Rules section to the tool. This enables us to define translation rules that map Event-B formulas to code. We illustrate the approach using a small case study, where we add a theory of arrays, and specify translation rules for generating Ada code.

Event-B is a state-based formal method that supports a refinement process in which an abstract model is elaborated towards an implementation in a step-wise manner. One weakness of Event-B is that control flow between events is typically modelled implicitly via variables and event guards. While this fits well with Event-B refinement, it can make models involving sequencing of events more difficult to specify and understand than if control flow was explicitly specified. New events may be introduced in Event-B refinement and these are often used to decompose the atomicity of an abstract event into a series of steps. A second weakness of Event-B is that there is no explicit link between such new events that represent a step in the decomposition of atomicity and the abstract event to which they contribute. To address these weaknesses, atomicity decomposition diagrams support the explicit modelling of control flow and refinement relationships for new events. In previous work, the atomicity decomposition approach has been evaluated manually in the development of two large case studies, a multi media protocol and a spacecraft sub-system. The evaluation results helped us to develop a systematic definition of the atomicity decomposition approach, and to develop a tool supporting the approach. In this paper we outline this systematic definition of the approach, the tool that supports it and evaluate the contribution that the tool makes.

This paper describes a formal modelling approach, where Ada code is automatically generated from the modelling artefacts. We introduce an implementation-level specification, Tasking Event-B, which is an extension to Event-B. Event-B is a formal method, that can be used to model safety-, and business-critical systems. The work may be of interest to a section of the Ada community who are interested in applying formal modelling techniques in their development process, and automatically generating Ada code from the model. We describe a streamlined process, where the abstract modelling artefacts map easily to Ada language constructs. Initial modelling takes place at a high level of abstraction. We then use refinement, decomposition, and finally implementation-level annotations, to generate Ada code. We provide a brief introduction to Event-B, before illustrating the new approach using small examples taken from a larger case study.

The construction of specifications is often a combination of smaller sub-components. Composition and decomposition are techniques that support reuse and allow us to formally combine sub-components through refinement steps while reusing their properties. Sub-components can result from a design or architectural goal and a refinement framework should allow further parallel development over the sub-components. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronisation over shared events and shared states are not allow. We define the necessary proof obligations to ensure a valid composition or decomposition. We also show that shared event composition preserves refinement proofs for sub-components, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding subcomponents. A case study applying these two techniques is illustrated using Rodin, the Event-B toolset.

Atomicity Decomposition is a technique in the Event-B formal method, which augments Event-B refinement with additional structuring in a diagrammatic notation to support complex refinement in Event-B. This paper presents an evaluation of Event-B atomicity decomposition technique in modeling a multi media case study with the diagrammatic notation. Firstly the existing technique and the diagrammatic notation are shown. Secondly an evaluation is performed by developing a model of a Media Channel System. A Media Channel is established between two endpoints for transferring multi-media data. Finally some extensions to the existing diagrammatic notation are proposed and applied to the multi-media case study.

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.

Event-B [1] is a formalism for discrete system modelling. The Rodin platform [2] 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.

UML-B is a ’UML-like’ graphical front end for Event-B that provides support for object-oriented modelling concepts. In particular, UML-B supports class diagrams and state machines, concepts that are not explicitly supported in plain Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same abstraction-refinement concepts can also be applied in UML-B. This paper introduces the notions of refined classes and refined state machines to enable refinement of classes and state machines in UML-B. Together with these notions, a technique for moving an event between classes to facilitate abstraction is also introduced. Our work makes explicit the structures of class and state machine refinement in UML-B. The UML-B drawing tool and Event-B translator are extended to support the new refinement concepts. A case study of an auto teller machine (ATM) is presented to demonstrate application and effectiveness of refined classes and refined state machines.

It is believed that reusability in formal development should reduce the time and cost of formal modelling within a production environment. Along with the ability to reuse formal models, it is desirable to avoid unnecessary re-proof when reusing models. Event-B is a formal method that allows modelling and refinement of systems. Event-B supports generic developments through the context construct. Nevertheless Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs.

Event-B is a formal method used for specifying and reasoning about systems. Rodin is a toolset for developing system models in Event-B. Our experiment which is outlined in this paper is aimed at applying Event-B and Rodin to a flash-based filestore. Refinement is a useful mechanism that allows developers to sharpen models step by step. Two uses of refinement, feature augmentation and structural refinement, were employed in our development. Event decomposition and machine decomposition are structural refinement techniques on which we focus in this work. We present an outline of a verified refinement chain for the flash filestore. We also outline evidence of the applicability of the method and tool together with some guidelines.

UML-B is a graphical formal modelling notation that relies on Event-B for its underlying semantics and is closely integrated with the `Rodin', Event-B verification tools. UML-B is similar to UML but has its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. When a UML-B drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram.The UML-B modelling environment consists of a UML-B project containing a UML-B model. Four interlinked diagram types (package, context, class and statemachine) are available. Package Diagrams are used to describe the `refines' and `sees' relationships between top level components (machines and contexts) of a UML-B project. UML-B mirrors the Event-B approach where static data (sets and constants) are modelled in a separate package called a `context'. The context diagram is similar to a class diagram but has only constant data represented by ClassTypes, Attributes and Associations.ClassTypes define `carrier' sets or constant subsets of other ClassTypes.

Event-B is a formalism used for specifying and reasoning about complex discrete systems. The Rodin platform is a new tool for specification, refinement and proof in Event-B. In this paper, we present a verified model of a tree-structured file system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities affecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a file system, we begin with an abstract model of a file system and subsequently refine it by adding more details through refinement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

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.

CDIS is a commercial air traffic information system that was developed using formal methods 15 years ago by Praxis, and it is still in operation today. This system is an example of an industrial scale system that has been developed using formal methods. In particular, the functional requirements of the system were specified using VVSL -- a variant of VDM. A subset of the original specification has been chosen to be reconstructed on the Rodin platform based on the new Event-B formalism. The goal of our reconstruction was to overcome three key difficulties of the original formalisation, namely the difficulty of comprehending the original specification, the lack of any mechanical proof of the consistency of the specification and the difficulty of dealing with distribution and atomicity refinement. In this paper we elucidate how a new formal notation and tool can help to overcome these difficulties. A Rodin archive of the project is also included. This may be imported to the Rodin tool.

ProB is an animation and model checking tool for the B Method, which can deal with many interesting specifications. Some specifications, however, contain complicated functions which cannot be represented explicitly by a tool. We present a scheme with which higher-order recursive functions can be encoded in B, and establish soundness of this scheme. We then describe a symbolic representation for such functions. This representation enables ProB to successfully animate and model check a new class of relevant specifications, where animation is especially important due to the involved nature of the specification.