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.