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

今天，许多制造业的产品，特别是航空航天、汽车和高科技制造业，都依赖于嵌入式软件的功能。由于这些产品中的许多都支持安全或关键任务服务，因此嵌入式软件的正确性是一个至关重要的问题。今天的大多数工业努力都集中在改进代码审查、测试和鉴定过程上，以实现这一目标。虽然这些过程可以揭示缺陷，但它们不能证明缺陷的存在。此外，在审查、测试甚至集成时发现缺陷已经太迟了。重大的工程工作已经发生，使进一步的改变变得复杂、昂贵和不确定。与测试方法相比，形式化验证可以证明软件的正确性，大大减少了测试的需要，同时也增加了可靠性。正式验证的研究已经进行了三十年，但在过去的几年里已经非常成熟。倡议者认为，现在有可能开发一个验证框架来验证模型驱动工程（MDE）符号，如UML和SysML，它们被广泛用于开发嵌入式软件。提议者先前已经将自定义符号中的MDE描述映射到源代码和进程代数CSP中，允许使用FDR进行正式验证，FDR也是提议者生成的模型检查器。这导致了包含100万行代码的经过验证的嵌入式系统。这项工作仅限于建模语言、系统架构和它所支持的执行语义，并且没有正式的证明来保证生成的源代码等同于被验证的模型。它也是一个点解决方案，不能与其他工具互操作，也不能处理遗留代码。这个建议的总体目标是产生一个工业上适用的框架，它支持MDE语言的验证和实现。我们还将开发一个概念验证工具，以支持我们的框架，并允许学术和工业开发。我们框架的核心将是一种新的形式化验证语言，称为通信组件（communication Components, CoCo），它被设计为用MDE语言编写的嵌入式软件建模。FDR将用于验证CoCo中表达的模型；FDR3最近的性能改进意味着我们将能够处理更复杂的组件和架构。我们还将提供从CoCo到源代码的翻译。我们将通过使用Coq定理证明器来证明翻译保留了模型的语义，从而提高源代码转换器的可靠性。除了MDE工程师将从该项目中受益外，形式方法研究人员也将受益。我们将基于我们在早期的验证工作中使用的组合方法，开发新的规范导向的抽象和验证技术。其次，我们将为FDR3添加额外的功能来支持这项工作，从而使我们的工作更容易被大型FDR3社区访问。我们聚集了一群热情的工业合作伙伴，包括航空航天技术研究所（英国航空航天战略的领导者），ASML（世界上最大的光刻系统供应商），ASTC（安全关键和实时控制电子工业工具和解决方案的全球行业领导者），MBDA（世界领先的导弹和导弹系统）和Rolls-Royce 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.