Scenario-based Consistency Testing Of Hybrid Automata

Hybrid systems are one kind of complex systems, which are often the core controllers of precision instruments and appear in many areas such as aerospace, train control and other safety-critical areas. Therefore, it shows great significance to study the quality assurance of hybrid systems. Hybrid automata are the main design modeling language of hybrid systems, and the existing researches are mainly focused on safety verification of hybrid automata. The hybrid automata, which contain both discrete and continuous dynamics, increase the complexity of the validation. For small linear hybrid systems, verification attempts to iterate through all the state space in order to check the safety of the systems. Verification cannot check complex nonlinear hybrid automata. The state space of the hybrid automata is very large and verification cannot deal with the problem. Existing work and techniques show poor performance on large-scale hybrid systems, and even the reachability of the linear hybrid automata (LHA), one simple kind of hybrid systems, cannot be decided.Verification cannot solve that problem and by now researchers have used a way of testing to check the safety of hybrid automata. But testing always focuses on whether some target points can be reached or not in the state space. In industrial applications, they not only need to check whether certain target points can be reached or not, but also need to check whether certain scenarios can be implemented or not. On the basis of techniques of testing before, this thesis has put forward the scenario-oriented test generation for hybrid automata and has designed and implemented the prototype tool. The details of the research in this thesis are as follows:· Present an algorithm of the scenario-oriented test generation of the single nonlin-ear hybrid automaton. This algorithm creates a discrete searching graph by the hybrid automata users input and builds a leading way. This thesis presents a new algorithm of construction of the scenario-oriented leading way and on the one hand this leading way can meet the requirements of the scenarios; on the other hand it can fully reach the target mode. Under the guide of the leading way, the system expands on the state space of hybrid automata to see whether the scenario events can occur or not. If they do occur and the system reaches the target points, the algorithm can generate test cases.· An algorithm is presented for the scenario-oriented test generation of the multiple nonlinear hybrid automata. Real systems always contain more than one hybrid automata. Hybrid automata combine different hybrid automata together which are connected by shared labels or events. Because of the introduction of the correlation between each other and the time requirements of synchronization events, this thesis introduces the situation of multiple automata. For this problem, this thesis presents the algorithm of the scenario-oriented test generation of the multiple nonlinear hybrid automata and generates test cases of multiple nonlinear hybrid automata.· By the techniques in this thesis a prototype tool for the scenario-oriented test generation of the hybrid automata has been developed and a case study has been carried out. It can solve the problems of the scenario-oriented test generation for both the single automaton and multiple automata and generate cases accordingly.