A formal verification method of hybrid system and simulation

Author

Si-bing, Zhang ; Chen Jie ; Ya, Wang

Author_Institution

Dept. of Sci. Res., Electron. Eng. Inst. of PLA, Hefei, China

Volume

4

fYear

2010

fDate

9-11 July 2010

Firstpage

411

Lastpage

415

Abstract

Hybrid system is a dynamic system that has discrete state transfer and continuous state variation. Recently, popular hybrid system model includes threshold-event-driven hybrid systems (TEDHS) and polyhedral invariant hybrid automaton (PIHA). Finite state machine is used to describe the discrete feature of hybrid system and reachable set of stream pipe is used to describe its continuity approximately. These methods of system modeling are given in this paper. Furthermore, a verification tool called CheckMate based on MATLAB is used to realize the modeling, simulation and verification of hybrid system.

Keywords

finite state machines; formal verification; CheckMate; MATLAB; continuous state variation; discrete state transfer; dynamic system; finite state machine; formal verification method; polyhedral invariant hybrid automaton; stream pipe; system modeling; threshold-event-driven hybrid system; verification tool; Analytical models; Artificial neural networks; Computer languages; Educational institutions; Mathematical model; Prototypes; CheckMate; finite automaton; hybrid system; stream pipe approximation;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Information Technology (ICCSIT), 2010 3rd IEEE International Conference on

Conference_Location

Chengdu

Print_ISBN

978-1-4244-5537-9

Type

conf

DOI

10.1109/ICCSIT.2010.5564050

Filename

5564050