Research On Formal Verification Methods For Hybrid Systems Based On Combined Formal Specification

Hybrid systems are state-transition systems consisiting of discrete control mode transformation and continuous real time behavior. Formal modeling and verification for hybrid systems are an important way to ensure the correctness and reliability of the systems. Hybrid systems exhibit not only complex dynamical behaviors and time constraints, but also communication with enviroment. So there is seldom works about a single specification technique that is well suited for all these aspects. Due to the infinite state-spaces of hybrid systems, the model checking problem and the reachability problem for most hybrid systems are undecidable.(1) In order to describe and verify all aspects of hybrid systems, this thesis firstly propose a specification model to describe data and behavioural of hybrid systems. This model, named multirate hybrid ZIA(MZIA), is a combination of interface automata, multirate hybrid automata and Z language.(2) Based on the continuous-time ZIA specification(CT-ZIA) proposed in article [27], this thesis propose a bisimulation relation on CT-ZIAs, which includes not only a bisimulation relation between behaviuoral properties, but a bisimulation relation between data structures properties. Then, to verify properties of CT-ZIAs, an algorithm for checking bisimulation relation between CT-ZIAs with finite domain is presented and the correctness is proven.(3) This thesis proposes a temporal logic with data constraints for MZIA. Considering the measuring errors of real-numbered variables in practice, this logic can describe that a MZIA specification approximatedly satisfies a given formula. Next, this thesis gives the approximated model checking algorithm for multirate hybrid systems, which can check whether a system described with MZIA satisfies the logic formula. At last, an example about boiler plant is given to indicate that this method is feasible and effective.(4) Finally, this thesis proposes a refinement relation on MZIAs, which includes not only an alternating simulation between behaviuoral properties, but a refinement relation between data structures properties. Then, an algorithm for checking refinement relation between MZIAs with finite domain is proposed, which can used to verify the correctness from specification to implementation automatically. An example about boiler plant is given to show the procedure of the algorithm.