TY - GEN
T1 - Formal verification and simulation
T2 - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
AU - Fang, Huixing
AU - Guo, Jian
AU - Zhu, Huibiao
AU - Shi, Jianqi
PY - 2012
Y1 - 2012
N2 - For hybrid systems, hybrid automata based tools are capable of verification while Matlab Simulink/Stateflow is proficient in simulation. In this paper, a methodology is developed in which the formal verification tool PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For application of this methodology, a Platform Screen Doors System (abbreviated as PSDS), a subsystem of the subway, is modeled with formal verification techniques based on hybrid automata and Matlab Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by PHAVer. It is verified that the sandwich situation can be avoided under time interval conditions. We conclude that this integration methodology is competent in verifying Platform Screen Doors System.
AB - For hybrid systems, hybrid automata based tools are capable of verification while Matlab Simulink/Stateflow is proficient in simulation. In this paper, a methodology is developed in which the formal verification tool PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For application of this methodology, a Platform Screen Doors System (abbreviated as PSDS), a subsystem of the subway, is modeled with formal verification techniques based on hybrid automata and Matlab Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by PHAVer. It is verified that the sandwich situation can be avoided under time interval conditions. We conclude that this integration methodology is competent in verifying Platform Screen Doors System.
KW - Formal Verification and Simulation
KW - Hybrid System
KW - Matlab Simulink/Stateflow
KW - PHAVer
KW - Subway Control System
UR - https://www.scopus.com/pages/publications/84866922844
U2 - 10.1109/TASE.2012.11
DO - 10.1109/TASE.2012.11
M3 - 会议稿件
AN - SCOPUS:84866922844
SN - 9780769547510
T3 - Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
SP - 145
EP - 152
BT - Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
Y2 - 4 July 2012 through 6 July 2012
ER -