Font Size: a A A

Analysis Of Linear Hybrid System Based On The Semantics Of Transition System

Posted on:2014-10-21Degree:MasterType:Thesis
Country:ChinaCandidate:H JiangFull Text:PDF
GTID:2308330482452249Subject:Computer technology
Abstract/Summary:PDF Full Text Request
Working as the core controller, hybrid system appears everywhere in the space transportation, machinery control and other safety-critical areas. Therefore, doing formal verification for the quality assurance of hybrid system shows important pratical significance. As hybrid automata is the main modelling language of hybrid system, the existing research has focused on the safety verification of hybrid automata. However, hybrid automata is very complicated for consisting of both discrete and continuous behaviors and is very hard to verify.Most existing techniques show poor performance on large scale systems. Even for the class of linear hybrid automata(LHA), the reachability verification problem is undecidable.In Contrast, transition system is a discrete system to discribe the jump relations between two states and its formal verification techniques are quite well developed. There are many off-the-shelf techniques and tools for analysis and verification of large scale transition systems. In fact, the state sequences of all kinds of formal model are performming transition relations between states essentially. Therefore, the paper toy to transform a LHA to an equivalent binary relational linear transition system(LTS), then take the advantage of the huge research achievement of LTS to achieve the large-seale verification of LHA on the multiple problems. The main contributions include:· Present the method of the construction from a LHA to an equivalent LTS and prove its equivalence. By introducing the variable t and self-loop transition on the location to express the state of the original system at anytime, the method successfully eliminate the quantifiers in the traditional expression by the semantics of transition system.· Based on the theoretical basis of above equivalent construnction, we take advantage of the existing technology of transition system to analysis the linear hybrid system on safety verification, liveness verification and stability analysis:。 Safety verification is carried out from proving reachability and we choose TS-oriented model checker ARMC. The experimental results demonstrate that the method can handle the large scale system very well compared with the existing techniques.。 Liveness verification is still a problem of LHA verification area and there is no relevant work commenced. We carry out the research from proving fair termination and we choose TS-oriented checker ARMC. The experimental results show that the method prove termination successfully and efficiently. This work is a breakthrough attempt in the related area.。Stability analysis is carried out from generating invariants and we choose two typical tools, Interproc and InvGen, corresponding to two typical frameworks, abstraction interpretation based and constraint solving based. We use the generated invariants to refine the original model automaticly. The experimental results show that the method can dig out a lot of hidden information for refinement and accelerate the follow-up work.
Keywords/Search Tags:Hybrid Automata, Transition System Construction Method, Safety, Liveness, Stability, Invariant Generation
PDF Full Text Request
Related items