Formal methods for safety critical real-time control systems

公共安全越来越依赖于汽车防抱死制动系统、飞机电传控制系统、医疗设备和其他系统的计算机控制系统的安全运行。这些系统依赖于软件的正确运行，为人类提供了以前无法想象的好处。因此，我们希望得到某种“证明”或“正式验证”，证明软件将正确运行，并且不会向公众开放。不幸的是，安全关键实时软件的构建和正式验证非常昂贵，需要经过专门培训的人员花费大量时间。因此，软件正确性的数学证明通常只有在监管机构授权确保公共安全的情况下，才被行业用于最安全关键的控制软件。为了使可证明正确的实时软件的构建不那么劳力密集，成本效益更高，拟议的研究将创建一个预先验证的软件组件库，以满足普遍存在的实时要求。该库将由软件组件和有关其属性的可移植定理组成。通过利用单个子组件的属性证明，工程师将能够轻松地证明较大组件的属性，因为它们是由子组件构建的。可移植定理将出现在基于XML的标准中，以允许使用多个验证环境，以便可以使用最合适的环境来建立设计的属性。定理证明器可以用来证明软件的逻辑正确性，而计算机代数系统可以用来检查软件如何与受控系统的连续动态相互作用。通过允许设计者在更高的层次上使用适当的工具进行推理，预验证的实时软件库将为更多的公司提供以更合理的成本创建经过正式验证的软件系统的可能性。

Increasingly public safety is dependent upon the safe operation of computer control systems in anti-lock brakeson cars, fly-by-wire controls on airplanes, medical devices and other systems. These systems rely upon thecorrect operation of their software to provide previously unimaginable benefits to humanity. Therefore wewould like to have some sort of "proof" or "formal verification" that the software will operate correctly and notendanger the public. Unfortunately, construction and formal verification of safety critical real-time software isvery costly, requiring significant time of specially trained personnel. As a result, mathematical proofs ofsoftware correctness are typically only used by industry in the most safety critical control software when it ismandated by a regulatory body to insure public safety. To make the construction of provably correct real-timesoftware less labour intensive and more cost effective, the proposed research will create a library ofpre-verified software components that meet commonly occurring real-time requirements. The library willconsist of software components and portable theorems about their properties. By leveraging the proofs of theproperties of the individual sub-components, engineers will be able to easily prove properties of largercomponents as they are constructed from the sub-components. The portable theorems will appear in an XMLbased standard to allow the use of multiple verification environments so that the most appropriate environmentcan be used to establish a property of a design. Theorem provers can be used for proofs of the software's logical correctness while computer algebra systems can be used to check how the software will interact with acontrolled system's continuous dynamics. By allowing the designers to reason at a higher level, using theappropriate tools, the pre-verified real-time software library will open up the possiblity of creating formallyverified software systems to more companies at a more reasonable cost.