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

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.

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