A Verified Multi-threaded Code Generation From Synchronous Programs

Real-time embedded systems in safety-critical domains such as aerospace are also considered as safety-critical systems,because malfunctions of these systems can lead to catastrophic accidents.At present,the industry widely approves that the model-driven(especially formal model-driven)development method is a practical and feasible method to design safety-critical systems.In particular,the model-based automatic code generation technology and related semantic preservation technology ensure the safety and reliability of the development process of these systems.As the functional requirements of safety-critical systems become increasingly complex,single-core processors are unable to meet the demands of higher computing performance of such systems,multi-core platforms that have advantages in terms of performance,size,weight,and power consumption(SWa P)are being widely used in safety-critical domains.Synchronous languages are a kind of formal languages that are very suitable for the design of safety-critical systems.As it becomes a trend that multi-core platforms are being widely applied in safety-critical systems,polychronous languages(such as SIGNAL)with multi-clock features have been attractive for embedded designer.The SIGNAL compiler supports to generate the sequential code and simulate experiments.The existing studies pay a little attention to the generation of multi-threaded code from SIGNAL specification.In addition,the SIGNAL compiler pays less attention to the semantic preservation of the code generation process.Therefore,this thesis proposes a multi-threaded code generation method and a related semantic preservation method for the synchronous language SIGNAL.The main contributions presented in the thesis can be summarized as follows:1)Proposing a multi-threaded code generation method for SIGNAL which includes four steps: program standardization(including lexical / parsing),clock calculus,task partition,and multi-threaded code generation.In the task partition phase,the thesis presents three task partition strategies to be suitable for different application scenarios: the basic task partition strategy,the topology-based task partition strategy,and the depth-first task partition strategy.In the multi-threaded code generation phase,the code generation phase is divided into platform-independent virtual multi-task structure generation and platform-dependent multi-threaded code generation(supporting multiple target languages: Ada / C / Java)in order to adapt to different software and hardware architectures of safety-critical systems.2)Proposing a semantic preservation method of multi-threaded code generation for SINGAL.The method consists of: the formal definition of the operational semantics of multiple intermediate languages in code generation,the formal description of algorithms and mapping rules in the code generation process,and the formal verification that the intermediate model retains the language characteristics of the source SIGNAL model like program termination and deterministic concurrency,and prove the semantic consistency between the SIGNAL program after clock calculus and the target C program after translation based on the bisimulation equivalent relation.3)Carrying out the case study with a real-world aerospace industrial case,the Guidance,Navigation and Control(GNC)system.The SIGNAL model of a GNC subsystem is used to show the feasibility of the multi-threaded code generation method presented in this thesis.And the experimental analysis on the multi-core platform leads to the following conclusions: When there is less synchronous communication in the SIGNAL model,the target program generated based on the depth-first task partition strategy performs more efficiently;and when there is more synchronous communication,the topology-based task partition strategy is more efficient.The SIGNAL multi-threaded code generation prototype tool is coded in the functional language OCaml,it is integrated into the Eclipse platform using the plug-in development technology.And the semantic preservation process is automatically checked by Coq Proof Assistant.Finally,the feasibility of the method proposed in this thesis is verified by a real-world industral cases.