Modeling and Verification of Cyber-physical Systems Based on Timed Automata
Zhihui Chen · Computer and Modernization · 2012
At present,the modeling and verification of Cyber-physical Systems(CPS) is becoming a hot topic of CPS software design.First,a typical prototype of CPS architecture is given and it generally consists of several basic components,e.g.,sensors,actuators,etc.Based on timed automata,CPS modeling approach is proposed,in which these components are modeled as individual timed automata reflecting their distributed and real-time characteristics.Then,all these time automata come into a network that represents concurrent communication and collaboration of the whole CPS.Finally,some properties(including time constraints) with the CPS are presented,and the correctness of the whole system is automatically verified by using the model-checking tool UPPAAL.