Certification of Safety-Critical Real-Time Systems

公共安全依赖于汽车、飞机、医疗设备和其他系统中的计算机控制系统的安全操作。这些系统依赖于其软件的正确操作来提供否则无法获得的好处。因此，我们需要“证明”软件将正确运行，不会危及公众。不幸的是，安全关键实时软件的构造、正式验证和由此产生的“认证”是非常昂贵的，需要训练有素的人员的大量时间，用于软件的生产及其认证。因此，软件正确性的数学证明通常仅在监管机构强制要求时才由行业在安全关键软件中使用。 更典型地，即使在安全关键应用中，软件的认证也是通过检查开发人员应用了基于标准的软件过程来完成的。为了降低实时软件的构建和以产品为中心的认证的劳动密集度并提高成本效益，拟议的研究将创建工具支持的方法和分析技术，以创建以产品为中心的认证证据，作为前瞻性软件开发过程的一部分。这项工作的一个关键特征是通过创建常用软件开发工具的扩展，将正式方法与实践工程师使用的工作流程和软件开发过程无缝集成。 特别是，我们将针对控制系统中使用的基于模型的设计工具，如Matlab/Simulink和MapleSim。这将通过使用领域特定语言来捕获模型的关键特征及其属性，然后将其转换为多个验证环境来实现，以便可以使用最合适的环境来建立设计的属性。通过允许设计人员在一个熟悉的环境中建模，然后在更高的层次上推理，使用正式的验证工具“引擎盖下”，我们打算开发一个控制系统设计模板库，有效地产生控制系统属性认证的证据，以更合理的成本，导致更可靠的软件密集型系统。

Public safety is dependent upon the safe operation of computer control systems in cars, airplanes, medical devices and other systems. These systems rely upon the correct operation of their software to provide otherwise unattainable benefits. Therefore we need to "certify" that the software will operate correctly and not endanger the public. Unfortunately, construction, formal verification and resulting "certification" of safety critical real-time software is very costly, requiring significant time of highly trained personnel, both for the production of the software and for its certification. As a result, mathematical proofs of software correctness are typically only used by industry in the safety critical software when it is mandated by a regulatory body. More typically, even in safety critical applications, a certification of the software is done by checking that a standards based software process was applied by developers. To make the construction and product-focused certification of real-time software less labour intensive and more cost effective, the proposed research will create tool supported methods and analysis techniques to create product focused evidence for certification as part of the forward software development process. A key feature of the work will be seamlessly integrating the formal methods with the work-flow and software development process used by practicing engineers by creating extensions to commonly used software development tools. In particular we will target model based design tools used in control systems such as Matlab/Simulink and MapleSim. This will be accomplished by the use of Domain Specific Languages to capture key features of the models and their properties and then allow their translation to multiple verification environments so that the most appropriate environment can be used to establish a property of a design. By allowing the designers to model in a familiar environment and then reason at a higher level, using the formal verification tools "under the hood", we intend to develop a library of control systems design templates that efficiently produce the evidence for certification of control systems properties at a more reasonable cost that results in more reliable software intensive systems.