Title
Modeling and checking for Cyber-Physical System based on hybrid interface automata
Abstract
Cyber-Physical Systems (CPS) are hybrid, safety-critical systems. For finding safety or security hazard in the design phase, modeling for CPS and checking their properties become very important. We focus on the compatibility, i.e., two systems can work together, and behavioral nonexistent consistency, i.e., forbidden behaviors do not occur in a system. Hybrid interface automata (HIA), which extend from interface automata and is not input-enabled, are introduced to model CPS. The compatibility of HIA is checked under an optimistic approach, which means if there is an environment in which two HIA cannot reach an illegal location, namely, at the location one cannot accept the input send by the other, they are compatible. Based on a scenario that specifies forbidden behaviors, behavioral nonexistent consistency is boundedly checked by transforming it to an unconstrained dynamic programming, and solving the programming by a genetic algorithm. The method can directly apply to nonlinear hybrid model. It relaxes a restriction on the form of the system dynamic in traditional algorithms. An experiment and simulation validate our algorithms.
Year
DOI
Venue
2015
10.1016/j.pmcj.2015.07.008
Pervasive and Mobile Computing
Keywords
Field
DocType
Cyber–Physical System,Hybrid system,Hybrid interface automaton,Scenario,Genetic algorithm
Dynamic programming,Nonlinear system,Compatibility (mechanics),Computer science,Automaton,Theoretical computer science,Cyber-physical system,Hybrid system,Genetic algorithm,Distributed computing
Journal
Volume
Issue
ISSN
24
C
1574-1192
Citations 
PageRank 
References 
2
0.49
20
Authors
5
Name
Order
Citations
PageRank
Yan Zhang131.18
Jin Shi2246.28
Tian Zhang311222.21
Xiangwei Liu430.85
Zhuzhong Qian538051.27