-
Article
Open AccessSystematic hierarchical analysis of requirements for critical systems
Safety and security are key considerations in the design of critical systems. Requirements analysis methods rely on the expertise and experience of human intervention to make critical judgements. While human j...
-
Chapter and Conference Paper
Semantics Formalisation – From Event-B Contexts to Theories
The Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TiMo) or State Chart XML (SCXML). Typically, the syntactical elements of the language...
-
Chapter and Conference Paper
Designing Exception Handling Using Event-B
The design of exception handling is a complex task requiring insight and domain expertise to ensure that potential abnormal conditions are identified and a recovery process is designed to return the system to ...
-
Chapter and Conference Paper
Develo** the UML-B Modelling Tools
UML-B is a UML-like diagrammatic front end for the Event-B formal modelling language. We have been develo** UML-B for over 20 years and it has gone through several iterations, each with significant changes o...
-
Chapter and Conference Paper
Building an Extensible Textual Framework for the Rodin Platform
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 th...
-
Chapter and Conference Paper
Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling
The increased complexity of high-consequence digital system designs with intricate interactions between numerous components has placed a greater need on ensuring that the design satisfies its intended requirem...
-
Chapter and Conference Paper
Designing Critical Systems Using Hierarchical STPA and Event-B
In the design of critical systems, it is important to ensure a degree of formality so that we reason about safety and security at early stages of analysis and design, rather than detect problems later. Influen...
-
Chapter and Conference Paper
Generating SPARK from Event-B, Providing Fundamental Safety and Security
Event-B is a formal method that facilitates rigorous analysis and correct-by-construction development of software and hardware systems. SPARK is a computer programming language for the development of high inte...
-
Chapter and Conference Paper
The CamilleX Framework for the Rodin Platform
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 th...
-
Chapter and Conference Paper
Refinable Record Structures in Formal Methods
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 us...
-
Chapter and Conference Paper
Extensible Record Structures in Event-B
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 ext...
-
Article
Open AccessFormalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B
We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach us...
-
Chapter and Conference Paper
Refinement and Verification of Responsive Control Systems
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 ...
-
Chapter
Systematic Verification and Testing
In this chapter, we present a process pattern for model based specification, verification and testing. It combines concepts of behaviour driven development (BDD), graphical and formal, mathematical modelling, ...
-
Chapter and Conference Paper
Formal Verification of Run-to-Completion Style Statecharts Using Event-B
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 ...
-
Chapter and Conference Paper
Domain-Specific Scenarios for Refinement-Based Methods
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 suffici...
-
Chapter and Conference Paper
Refinement of Statecharts with Run-to-Completion Semantics
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 refinemen...
-
Chapter and Conference Paper
A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods
Formal methods (in a broad sense) have been around almost since the beginning of computer science. Nonetheless, there is a perception in the formal methods community that take-up by industry is low considering...
-
Chapter and Conference Paper
Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3
We demonstrate diagrammatic Event-B formal modelling of a hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. We perform a re...
-
Chapter and Conference Paper
Behaviour-Driven Formal Model Development
Formal systems modelling offers a rigorous system-level analysis resulting in a precise and reliable specification. However, some issues remain: Modellers need to understand the requirements in order to formul...
