Formal methods for safety critical real-time control systems

点击翻译按钮获取中文摘要

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.