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