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.
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. 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.
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.
Publications
Antonino P
(2019)
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
in Formal Aspects of Computing
Antonino P
(2016)
Integrated Formal Methods
Antonino P
(2017)
Formal Methods: Foundations and Applications
Antonino P
(2019)
Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving
in ACM Transactions on Software Engineering and Methodology
Boulgakov A
(2016)
Computing maximal weak and other bisimulations
in Formal Aspects of Computing
Brookes S
(2021)
Theories of Programming - The Life and Works of Tony Hoare
Gibson-Robinson T
(2017)
Concurrency, Security, and Puzzles
Gibson-Robinson T
(2019)
Symmetry reduction in CSP model checking
in International Journal on Software Tools for Technology Transfer
Mestel D
(2020)
Translating between models of concurrency
in Acta Informatica
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 has several more clients. For the last two years Cocotec has had 6 full time staff. As of February 2023 Cocotec continues to be very successful with its product in daily use by hundreds of engineers in industry. |
First Year Of Impact | 2019 |
Sector | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),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 |
Description | Cocotec develops a model checker for the development of complex aerospace industrial software. |
Year Established | 2016 |
Impact | Software is in significant use by ASML: see https://www.linkedin.com/pulse/computers-improving-scanner-metrology-software-code-lewis There are other smaller customers, |
Website | http://www.cocotec.io |