EPSRC Industrial Case Grant EP/J501992

The Development of Rigorous Methods for the Design of Complex Systems, in line with Military and Civil Standards for Complex Hardware and Software.

Project Team

Andrew Ireland [ Principal Investigator ] (Heriot-Watt University) 
Rajiv Murali [ Research Student ] (Heriot-Watt University) 
Gudmund Grov [ Collaborator ] (Heriot-Watt University) 
Benjamin Gorry [Industrial Partner] (BAE Systems) 

Research
This project has investigated an approach to embedding formal methods within UML use case modelling. The formal method of interest is Event-B, which is refinement based and consequently has enabled us to exploit a natural abstractions found within UML use cases. By underpinning informal use cases with Event-B, we are able to provide greater precision and formal assurance when reasoning about concerns identified by system engineers as well as the subsequent changes made at the level of use case modelling.

Publications
Rajiv Murali, Andrew Ireland and Gudmund Grov. "UC-B: Use Case Modelling with Event-B", 5th International ABZ Conference (ABZ 2016).

Rajiv Murali, Andrew Ireland and Gudmund Grov. "A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios", 7th NASA Formal Methods Symposium (NFM 2015).

Rajiv Murali and Andrew Ireland. "E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs", Automated Verification of Critical Systems (AVoCS'2012).

UC-B Tool Development
UC-B (Use case Event-B) supports the authoring and management of UML use case models on Event-B's Rodin platform. Its purpose is to extend UML use cases by allowing its specification to be detailed with both informal and formal notation. Formal notation is written with Event-B's mathematical language, which is based on set theory that allow precise descriptions of intended system behaviour to be written in an abstract way. Once the use cases are detailed the tool supports the automatic generation of corresponding Event-B models. Event-B's verification tools (syntax checks and provers) then run automatically providing an immediate display of problems which can be related back to the use case model.