EPSRC logo

Details of Grant 

EPSRC Reference: EP/Y001532/1
Title: Exploring Theories and Semantics in Event-B
Principal Investigator: Farrell, Dr M
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Manchester, The
Scheme: Standard Research - NR1
Starts: 11 December 2023 Ends: 10 June 2025 Value (£): 165,304
EPSRC Research Topic Classifications:
Computer Sys. & Architecture Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
17 May 2023 ECR International Collaboration Grants Panel 1 Announced
Summary on Grant Application Form
From autonomous robotics to driverless cars, we are encountering increasingly complex and safety-critical systems in our daily lives. It is natural to want to ensure that these systems behave correctly and safely in any given scenario. Formal methods are a set of mathematically-based techniques for the specification and verification of software systems. These methods provide developers with the tools and techniques needed to verify and ensure the correctness of safety-critical software. However, we must also ensure that the formal methods themselves (and the features that they provide) are robust, transparent and well-defined.

Event-B is an industrial-strength formal specification language for the development of safety-critical systems. These systems include aerospace, rail, healthcare and robotic applications. To be capable of being adopted in the development of increasingly complex systems, formal methods must support standard software engineering practices such as modularity. Such formal methods should also be equipped with a detailed semantics so that the results are interpreted correctly by both software engineers as well as interoperable tools.

Although used extensively in industry, Event-B currently lacks robust theoretical foundations to support modular specifications and interoperability between other specification languages as well as general programming paradigms. These features are becoming necessary as systems increase in both size and complexity. A prime example concerns the robotics domain where systems comprise a combination of distinct modules that may be written and reasoned about using a heterogeneous set of programming languages and logics.

Recently, both theory and tools have been developed that provide a basis for the addition of modularistation constructs and multi-logic support to Event-B specifications. First is the algebraic semantics devised by Farrell et al., which also defines modularisation constructs, called specification-building operators, and pathways to interoperability for Event-B models. Second, the EB4EB framework which defines a meta-theory (based on proof obligations) for Event-B that enables specification and verification of extensions to the Event-B language. This collaboration seeks to unify these two distinct threads of research.

Specifically, it will focus on developing the capability to manipulate and reason about Event-B structures and their associated semantics in a unified setting using the EB4EB framework. We will encode the support for modularisation from Farrell's algebraic semantics (EVT) using EB4EB and demonstrate how this can capture (and is more general than) the current (shallow) approaches to providing modular specification for Event-B. This shallow modularity is typically achieved via the development of plugins for the Event-B IDE, the Rodin Platform, such as the composition/decomposition plugins. Since heterogeneous specification is desired in complex safety-critical systems such as robotics, we will also investigate how the approach to interoperability in the algebraic semantics can be implemented in EB4EB to support specification and verification of hybrid systems.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.man.ac.uk