EPSRC logo

Details of Grant 

EPSRC Reference: EP/N022777/1
Title: Reducing Cost of Software: A Scalable Model-Based Verification Framework
Principal Investigator: Roscoe, Professor A
Other Investigators:
Researcher Co-Investigators:
Dr P Hopcroft
Project Partners:
ASML ASTC Rolls-Royce Plc
Department: Computer Science
Organisation: University of Oxford
Scheme: Standard Research
Starts: 01 May 2016 Ends: 30 June 2019 Value (£): 961,156
EPSRC Research Topic Classifications:
Computer Sys. & Architecture
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:
Panel DatePanel NameOutcome
09 Feb 2016 Engineering Prioritisation Panel Meeting 9 and 10 February 2016 Announced
Summary on Grant Application Form
Today's products from many manufacturing industries, notably aerospace,

automotive and high-tech manufacturing, depend on embedded software to

function. Since many of these products support safety or mission-critical

services, the correctness of the embedded software is a paramount concern. Most

of today's industrial efforts focus on improving the code review, testing and

qualification process to achieve this. Whilst these processes can reveal

defects, they cannot prove their absence. Further, finding defects at review,

test or even integration time is too late. Significant engineering efforts have

already occurred, making further changes complicated, costly, and uncertain.

In contrast to testing approaches, formal verification can prove the

correctness of software, substantially reducing the need for testing, whilst

also increasing reliability. Formal verification has been investigated for

three decades, but has matured significantly over the last few years. The

proposers believe it is now possible to develop a verification framework that

can verify Model-Driven Engineering (MDE) notations such as UML and SysML,

which are widely used to develop embedded software.

The proposers have previously mapped MDE descriptions in a custom notation into

both source code and the process algebra CSP, allowing formal verification

using FDR, a model checker also produced by the proposers. This led to verified

embedded systems that contained 1M lines of code. This work was limited in the

modelling languages, the system architectures, and execution semantics it

supported and had no formal proof guaranteeing the source code generated was

equivalent to the models being verified. It was also a point solution that

could not interoperate with other tools, nor handle legacy code.

The overall goal of this proposal is to produce an industrially-applicable

framework that supports verification and implementation of MDE languages. We

will also develop a proof-of-concept tool that supports our framework and

allows both academic and industrial exploitation.

At the core of our framework will be a new formal verification language, called

Communicating Components (CoCo), that is designed to model embedded software

written in MDE languages. FDR will be used to verify models expressed in CoCo;

the recent step-change performance improvements in FDR3 mean we will be able to

handle more complex components and architectures. We will also provide a

translation from CoCo into source code. We will improve the reliability of the

source code translator by using the Coq theorem prover to prove the translation

preserves the semantics of the model.

In addition to the MDE engineers who will benefit from this project, formal

methods researchers will also benefit. We will develop new

specification-directed abstraction and verification techniques, based on the

compositional methods we used in our earlier verification work. Secondly, we

will add extra functionality to FDR3 to support this work, and thereby make our

work readily accessible to the large FDR3 community.

We have assembled an enthusiastic group of industrial partners comprising

Aerospace Technology Institute (leader of UK strategy for aerospace), ASML

(world's largest supplier of photolithography systems), ASTC (global industry

leader for tools and solutions in safety critical and real time control

electronics industries), MBDA (world leader in missiles and missile systems)

and Rolls-Royce CDS (leading provider of high integrity control systems), who

will collaborate with us and provide essential industrial expertise across

these industries. This will allow us to ensure that the framework and

proof-of-concept tool we produce are industrially applicable. Our partners will

also provide case studies and, we hope, ultimately provide users for our


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.ox.ac.uk