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

今天，许多制造业的产品，特别是航空航天、汽车和高科技制造业的产品，都依赖于嵌入式软件来发挥作用。由于这些产品中的许多都支持安全或任务关键型服务，因此嵌入式软件的正确性是最重要的问题。今天的大多数工业努力都集中在改进代码审查、测试和鉴定过程以实现这一点。虽然这些过程可以揭示缺陷，但它们不能证明它们的缺失。此外，在审查、测试甚至集成时间发现缺陷已经太晚了。已经进行了大量的工程工作，这使得进一步的更改变得复杂、昂贵和不确定。与测试方法相比，正式验证可以证明软件的正确性，大大减少了测试需要，同时也增加了可靠性。正式核查已被研究了三十年，但在过去几年中已显著成熟。提出者认为现在有可能开发一种验证框架来验证被广泛用于嵌入式软件开发的模型驱动工程(Model-Driven Engineering，MDE)符号，如UML和SysML，并将MDE描述以自定义符号映射到源代码和进程代数CSP中，从而可以使用FDR进行形式化验证，FDR也是提出者开发的模型检查器。这导致了经过验证的包含100万行代码的嵌入式系统。这项工作仅限于建模语言、系统架构和它所支持的执行语义，并且没有正式的证据来保证生成的源代码与被验证的模型是等价的。它也是一个点解决方案，不能与其他工具互操作，也不能处理遗留代码。这项提议的总体目标是产生一个支持MDE语言验证和实施的工业适用框架。我们还将开发一个概念验证工具，它支持我们的框架并允许学术和工业开发。我们框架的核心将是一种新的形式化验证语言，称为通信组件(COCO)，它旨在对用MDE语言编写的嵌入式软件进行建模。FDR将用于验证用COCO表示的模型；FDR3中最近的步长变化性能改进意味着我们将能够处理更复杂的组件和体系结构。我们还将提供从可可到源代码的翻译。我们将通过使用CoQ定理证明器来证明源代码翻译器保留了模型的语义，从而提高了源代码翻译器的可靠性。除了将从该项目中受益的MDE工程师，形式方法研究人员也将受益。我们将在早期验证工作中使用的组成方法的基础上，开发新的规范指导的抽象和验证技术。其次，我们将在FDR3中增加额外的功能来支持这项工作，从而使更多的FDR3社区能够轻松地访问我们的工作。我们已经组建了一批热情的工业合作伙伴，包括航空航天技术研究所(英国航空航天战略的领导者)、ASML(全球最大的光刻系统供应商)、ASTC(全球安全关键与实时控制电子行业工具和解决方案的行业领先者)、MBDA(导弹及导弹系统的世界领先者)和罗尔斯-罗伊斯CDS(高完整性控制系统的领先供应商)，他们将与我们合作，提供这些行业必不可少的工业专业知识。这将使我们能够确保我们生产的框架和概念验证工具在工业上适用。我们的合作伙伴还将提供案例研究，并希望最终为我们的技术提供用户。

Today's products from many manufacturing industries, notably aerospace,automotive and high-tech manufacturing, depend on embedded software tofunction. Since many of these products support safety or mission-criticalservices, the correctness of the embedded software is a paramount concern. Mostof today's industrial efforts focus on improving the code review, testing andqualification process to achieve this. Whilst these processes can revealdefects, they cannot prove their absence. Further, finding defects at review,test or even integration time is too late. Significant engineering efforts havealready occurred, making further changes complicated, costly, and uncertain.In contrast to testing approaches, formal verification can prove thecorrectness of software, substantially reducing the need for testing, whilstalso increasing reliability. Formal verification has been investigated forthree decades, but has matured significantly over the last few years. Theproposers believe it is now possible to develop a verification framework thatcan 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 intoboth source code and the process algebra CSP, allowing formal verificationusing FDR, a model checker also produced by the proposers. This led to verifiedembedded systems that contained 1M lines of code. This work was limited in themodelling languages, the system architectures, and execution semantics itsupported and had no formal proof guaranteeing the source code generated wasequivalent to the models being verified. It was also a point solution thatcould not interoperate with other tools, nor handle legacy code.The overall goal of this proposal is to produce an industrially-applicableframework that supports verification and implementation of MDE languages. Wewill also develop a proof-of-concept tool that supports our framework andallows both academic and industrial exploitation.At the core of our framework will be a new formal verification language, calledCommunicating Components (CoCo), that is designed to model embedded softwarewritten 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 tohandle more complex components and architectures. We will also provide atranslation from CoCo into source code. We will improve the reliability of thesource code translator by using the Coq theorem prover to prove the translationpreserves the semantics of the model.In addition to the MDE engineers who will benefit from this project, formalmethods researchers will also benefit. We will develop newspecification-directed abstraction and verification techniques, based on thecompositional methods we used in our earlier verification work. Secondly, wewill add extra functionality to FDR3 to support this work, and thereby make ourwork readily accessible to the large FDR3 community.We have assembled an enthusiastic group of industrial partners comprisingAerospace Technology Institute (leader of UK strategy for aerospace), ASML(world's largest supplier of photolithography systems), ASTC (global industryleader for tools and solutions in safety critical and real time controlelectronics industries), MBDA (world leader in missiles and missile systems)and Rolls-Royce CDS (leading provider of high integrity control systems), whowill collaborate with us and provide essential industrial expertise acrossthese industries. This will allow us to ensure that the framework andproof-of-concept tool we produce are industrially applicable. Our partners willalso provide case studies and, we hope, ultimately provide users for ourtechnology.