SACRES: A Step Ahead in the Development of Critical Avionics Applications

摘要

Basically, aircrafte engines can be divided into a control embedded system and a controlled system with its environment. The behaviour fo jthe controlled system is given a priori, while the control system still needs to be designed in a way guaranteeing the correct overall behaviour under all operational conditions depending on the flight domain. A large quantity of functions in ocntrol systems can be described by a formal system expressed in block diagrams and state-based represen-tations. These representations can be translated to formal based tools relying on the synchronous languages signal and statecharts. SACRES is a tool set supporting the design of safety-critical embedded control systems. It integrates the tools and specification techniques statemate, sildex, and Timing Diagrams with tool comp9onents for automatic code generation, formal verification based on model checking techniques, and an innovative approach for automatic code validation for target code generated from DC+. Technical achievements are-Integration of dataflow and state-based specification styles-Formal specification of safety-critical properties-Integration of efficient symbolic model checking techniques with statemate and sildex-Automatic generation of efficient distributed code-Automated correctness proofs for the generated code.