Simulation And Verification Of Spatial-Temporal Consistence Agent Modelling And Monitoring Based On STeC Language

With the development of webification, systematization, informationization and other features of Cyber Physical Systems, software systems become increasingly complex and compositive. Particularly the introduction of temporal, spatial and other physical elements provide new challenge for formal modelling methods. Recently, Professor Chen Yixiang introduced a specification language STeC (Spatio-temporal Consistence Language for Real-time Systems). STeC language is a specification language for Cyber Physical Systems, can build formal models for real-time systems directly and accurately, and stresses the spatio-temporal consistence for real-time systems.Firstly, this thesis aimed at an instance of spatio-temporal agent, Jinghu Gaotie (high speed rail train), used STeC language to build formal models. This thsis established a STeC to Stateflow automatic transformation system, proposed a simulation and verification approach based on STeC language and this transformation system. It gave a formal model for an object system in STeC specification language, and set up a real-time monitoring simulation model using Simulink. After that, it presented a verification approach for the system safety property based on Checkmate. This approach was used to static analyze a case of Jinghu Gaotie. The model checking results verified the system’s safety. Static simulation results met the needs of practical application.Secondly, this thesis focused on dynamic monitoring of high speed train. Specification language STeC was used to build formal models. We provided and used a series of specific monitoring methods to simulate and analyze this case. The methods provide feasible dynamic monitoring solutions, satisfied the system requirements of spatial-temporal consistence.At last, this thesis designed and developed a STeC dynamic simulation and evolution software system. This software used specification language STeC to build formal models, integrated and realized the above mentioned automatic transformation systems, static analysis functions and dynamic monitoring functions. This software was used for modelling and analysis of spatial-temporal consistence agents, fitted good design patterns, had high graphical usability and flexible reusability.