Paper Info
Title
Verification of rectangular hybrid automata models
Abstract
Formal analysis of hybrid systems is concerned with verifying whether a hybrid system satisfies a desired specification, like avoiding an unsafe region of the state space. For safety, economical and performance reasons, the satisfaction of critical design specifications of hybrid systems must be verified before embarking into their expensive construction and operation. Verification approaches based on system modelling with rectangular hybrid automata can lead to decidable solutions that find an algorithm which searches for the existence of states in the model which can be associated with the design specifications. This search is usually computation time intensive and after the elapse of a significant portion of time the user is unable to judge whether the state of interest is not reachable or the algorithm requires more time to terminate. In this work an algorithm, which alleviates the drawback of state space search, is proposed. Analytic approximations are used to express the time period the automaton stays at each one of its vertices in terms of the number of automaton iterations required to reach a desired state. Solving these relationships, one can find out whether the state of the model is reachable after a finite number of iterations. A case study is also presented that demonstrates the application of the algorithm to the verification of the operating specifications of a chemical reaction process that is controlled by a computer.
Year
DOI
Venue
2006
10.1016/j.jss.2006.01.016
Journal of Systems and Software
Keywords
Field
DocType
Formal methods,Rectangular hybrid automata,Specification verification,Hybrid systems
Computer science,Automaton,Algorithm,Decidability,State space search,Formal methods,Hybrid system,State space,Computation,Formal verification
Journal
Volume
Issue
ISSN
79
10
0164-1212
Citations 
PageRank 
References 
3
0.45
17
Authors
2
Name
Order
Citations
PageRank
Isabella Kotini171.90
George Hassapis26910.92