| 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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| 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 |