Certification of Safety-Critical Real-Time Systems

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

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.