Modeling And Analysis Of Embedded Periodic Control Systems

Embedded periodic control systems that are widely used in safety-critical embedded domains, such as automotive and avionics control, usually reveal periodic behaviors. Such periodic control systems share some interesting features and characteristics.(1) mode-based. A periodic control system is usually composed of a set of modes, with each mode representing an important state of the system. Each mode either contains a set of sub-modes or performs controlled computation periodically.(2) computation-oriented. In each mode, a periodic control system may perform control algorithms involving complex computation. For instance, in certain mode, a automotive control system may need to process intensive data in order to decide its location.(3) periodically. A periodic control system is reactive and may run for a long time. The behavior of each mode is regulated by its own period. That is, most computations are performed within a period and may be repeated in the next period if mode switch does not take place. Mode switch may only take place at the end of a period under certain conditions.Despite the fact that periodic control systems have been widely used in areas such as spacecraft control, there is lack of a concise and precise domain specific formal modelling language for such systems. In our research project supported by NSFC, we have started with several existing modelling languages but they are either too complicated therefore require too big a learning curve for domain engineers, or are too specific/general, therefore require non-trivial restrictions or extensions. A new formal but lightweight modelling framework SPARDL that matches exactly the need of the domain engineers is proposed from these motivations. The SPARDL framework is composed by two main aspects, the modelling notation ModeDiagram (MD for short) and the specification language SRDL.Although the proposed modelling notation MD can be regarded as a variant of S-tatecharts [56], it has been specifically designed to cater for the domain-specific need in modelling periodic control systems. The key part of a SPARDL model is the collection of modes given in the mode level. Each mode has a period, and the periods for different modes can be different. A mode can be nested and the transitions between modes or sub-modes may take place. A transition may be enabled if the associated guard is satisfied. In SPARDL, the transition guards may involve complex temporal expressions.An MD model is presented hierarchically. A mode that does not contain any sub-modes (termed a leaf mode) contains a control flow graph (CFG) encapsulating specific control algorithms or computation tasks. The details of CFGs are given in the CFG level. The CFGs may refer to modules (similar to procedures in conventional languages) details of which are given in the module level.To support formal reasoning about SPARDL models, we also provide a property specification language inspired by an interval-like calculus [42], which facilitates the cap-ture of temporal properties system engineers may be interested in.To reason about whether an SPARDL model satisfies desired properties specified by system engineers using the property specification language, we employ statistical model checking techniques [125,126]. Since SPARDL may involve complex non-linear com-putation in its flow graph, the complete verification is undecidable.In summary, the following contributions have been made in this paper:●A novel visual formal modelling framework SPARDL is proposed as a concise yet precise modelling language for embedded periodic control systems.●Two approaches are proposed to develop the formal semantics for SPARDL, one is the translation from SPARDL to priced timed automata and the other is an op-erational semantics interpreted on labelled transition systems. Type-safety, bi-simulation and equivalence are also discussed based on operational semantics.●Based on its formal semantics, the simulation of SPARDL is implemented and the stochastic semantics is developed. Guided from the stochastic semantics, a simulation-based statistical model checking algorithm is developed to verify S-PARDL models against various temporal properties.●Real life case studies have been carried to demonstrate the effectiveness of the pro-posed framework. We have managed to discover some design defects of a control system used in industry.