Reducing Cost of Software: A Scalable Model-Based Verification Framework

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

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
technology.

Planned Impact

This project will create an ECONOMIC impact to the UK by reducing the cost of
embedded software development, a key concern for many manufacturing industries.
The cost of embedded software development is continuing to rise and, in a
recent report, the Carnegie Mellon Software Engineering Institute estimated
that in aerospace the 'software affordability limit' has already been reached.
This means that aerospace is no-longer able to develop embedded software whilst
keeping costs to reasonable levels, dramatically affecting the industry's
ability to innovate. Aerospace is a key sector in the UK economy, and exports
£10.5 billion from the UK each year.

This project aims to reduce the cost of embedded software development for
manufacturing industries by utilising formal verification. This has the
potential to reduce costs primarily because it will reduce the amount of
testing required, which can consume up to 80% of development costs. In
addition, it will reduce the large cost associated with the discovery of
software bugs late in the development process, since software will be formally
verified throughout the development process.

This project will also enable manufacturing industries who use embedded
software to be more innovative. This is particularly true of manufacturers of
safety-critical devices, where the testability of software restricts the
developers to only consider features that can be tested in an affordable
manner. Allowing manufacturing industries to be more innovative will further
enable such companies to be more profitable.

The project will also make a SOCIETAL impact, since the general public will
ultimately use the products that are produced by the users of our formal
verification tools. For example, embedded software appears in everything from
medical devices such a pacemakers through to cars. These resulting products
should be more reliable and, in the case of safety-critical embedded software,
less likely to fail in potentially dangerous ways. Gien the increasing number
of day-to-day devices that embedded software is being incorporated into, we
anticipate that the safety (and security) of embedded software is likely to
become a significant concern to society within the next decade.
 
Description We have developed a new framework called Coco for developing proved embedded software from UML descriptions.
Exploitation Route People can build new Coco tools or ones that link to ours.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Healthcare

 
Description The Coco System is the basis of the Cocotec Spin-Out which went into fully-active mode when the main staff transferred into it at the end of the contract. The system has been adopted on a large scale by ASML and is under trial by a number of other companies.
First Year Of Impact 2019
Sector Aerospace, Defence and Marine,Manufacturing, including Industrial Biotechology
Impact Types Economic

 
Description Aerospace Technology Institute 
Organisation Aerospace Technology Institute
Country United Kingdom 
Sector Charity/Non Profit 
PI Contribution We have received additional funding of 300K (part of a grant also covering another Oxford Group) to liaise with Aerospace companies and integrate our solutions with their tools and processes
Collaborator Contribution Additional use cases and requirements.
Impact Collaboration is at an early stage: we have just appointed a researcher with ATI's money
Start Year 2016
 
Description Collaboration with ASML 
Organisation ASML Holding
Country Netherlands 
Sector Private 
PI Contribution Our EPSRC project, plus additional funding from Oxford and ASML, is helping us liaise on the improvement of their software development project. We are developing new techniques for creating verified embedded software as used in their hugely complex products
Collaborator Contribution Funding, plus personnel working with us, and active discussions about the verification challenges they face.
Impact We are having a significant impact on ASML's planning for its future software development.
Start Year 2016
 
Description Draper 
Organisation Draper Laboratory
Country United States 
Sector Charity/Non Profit 
PI Contribution Draper are substantial users of FDR, generally in projects related to the US Military. We advise them on this use.
Collaborator Contribution Practical problems driving FDR development It is through Draper that we obtained nearly $1.3M DARPA funding to develop FDR3 and its use.
Impact FDR has been employed by Draper to verify several pieces of US Military hardware, for example for the Navy. The details of this work are classified or confidential.
 
Description MBDA 
Organisation MBDA Missile Systems
Department MBDA UK Ltd
Country United Kingdom 
Sector Private 
PI Contribution We are working with MBDA on the potential use of our outputs in the creation of embedded software
Collaborator Contribution We have engaged in several meetings with them
Impact This collaboration is at an early stage
Start Year 2016
 
Description Rolls Royce 
Organisation Rolls Royce Group Plc
Country United Kingdom 
Sector Private 
PI Contribution We are working with Rolls Royce to integrate our embedded software development methods into their process.
Collaborator Contribution The is at an early stage, Several meetings have taken lpace.
Impact Early stage
Start Year 2016
 
Description  
IP Reference  
Protection Copyrighted (e.g. software)
Year Protection Granted
Licensed Yes
Impact Cocotec Ltd has become an Oxford spin-out with results of this project licenced. Will be launched during 2019
 
Title Coco System 
Description Software for verifying and generating embedded software from models in notations including UML 
Type Of Technology Software 
Year Produced 2019 
Impact Used by ASML and other companies 
 
Company Name COCOTEC LIMITED 
Description Company set up to exploit the ideas that led to this grant, namely automatic generation and verification of embedded software. Has now become official Oxford Spin-out and will take up the work of this contract when it is finished. Now the research project is complete (as of summer 2019) the two principal staff on that project are working full-time in the spin-out, and software (for the automated verification and generation of embedded software) is being used by customers. The company has some funding from the Aerospace Technology Institute (Innovate UK). 
Year Established 2016 
Impact Software is in significant use by ASML and in the process of assessment by other potential customers.