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.