Modeling and Analysis of Hybrid Control Systems An Elevator Case Study
Ying Zhang, Alan K. Mackworth · 1999
Summary, We propose a formal approach to the modeling and analysis of hybrid control systems. The approach consists of the interleaved phases of hybrid dynamic system model ing, requirements specification, hybrid control design and overall behavior verification. We have developed Constraint Nets as a semantic model for hybrid dynamic systems. Using this model, continuous, discrete and event-driven components of a dynamic system can be rep resented uniformly. We have developed timed \;;I-automata as a requirements specification language for dynamic behaviors. Using this language, many important properties of a dy namic system, such as safety, stability, reachability and real-time response can be formally stated. We have also proposed a verification method for checking whether a constraint net model satisfies a timed \;;I-automaton specification. The method uses the induction principle and generalizes both Liapunov stability analysis for dynamic systems and monotonicity of well-foundedness in discrete-event systems. The power of these techniques is demonstrated with a simple elevator system. An elevator system is a typical hybrid system with continu ous motion following Newtonian dynamics and discrete event control responding to users' request. We model the complete elevator system using Constraint Nets and verify the overall behavior of the system against the requirements specification in timed \;;I-automata.