Software Tool-Chain For The Design And Analysis Of Hybrid Embedded Systems

To settle the design complexity in the development of embedded systems, hybrid automata are introduced to model the behavior of embedded systems, then a tool-chain for the modeling, simulation and analysis of hybrid systems using the model-integrated computing framework is constructed. In this tool-chain, the generic semantic unit and the domain-specific modeling languages for hybrid automata are formally defined. The model transformations rules are constructed for the transformations between different modeling languages. With the effort of this tool-chain, hybrid systems can be modeled for the simulation purpose and transformed into the analysis models. The analysis models can be mapped to the executable code by a code generator, then, the executable code invokes the level set kernel for analyzing the reachable set of hybrid systems.To verify the correctness of model transformation rules, a framework for checking the bisimulation relation between models in the model transformation rules for hybrid automata models is proposed. For verifying whether the model transformation rules transform the input models into the output models correctly or not for every instant execution, this framework checks the bisimulation relation between the input models and output models. If the bisimulation relation holds, then this framework could conclude that the execution of the model transformation rules for these input model and output model is correct. A bisimulation checker is constructed based on the proposed framework for the correctness checking for the model transformation rules of hybrid automata models. This bisimulation checker could generate the checking conditions and algorithm for bisimulation through the elements mapping between the input models and output models, after each execution of model transformation rules, the checker could automatically check whether the bisimulation relation holds or not.As a case study, the power transient system of the Single Machine-Infinite Bus (SMIB) system is constructed in our tool-chain. The bisimulation relation between the input model and output model of model transformation rules for power transient system is checked by the bisimulation checker. We also perform reachability computation for it in our ReachLab analysis platform by using the forward reachability algorithm and the Box and Diamond iterative computation algorithm for the reachable sets and stability region of the power transient system.The software tool-chain for hybrid embedded systems developed in this thesis can be used to model and simulate the hybrid embedded systems efficiently and support the analysis of hybrid embedded systems through different analysis algorithm. This could ensure that the constructions of hybrid embedded systems are correct in the early stage of system modeling.