Formal verification of discrete event and hybrid systems
Sonia R. Sachs · 1996
Systems theory has traditionally been engaged in the modeling of dynamical systems. Ordinary or partial differential (difference) equation mathematical models have been successfully used to represent the evolution of continuous variable dynamical systems in continuous or in discrete time. However, as computers became essential components of most systems, the traditional mathematical representation of systems became inadequate. The state variables of such systems also take values from symbolic or logical domains. State changes may occur due to non-deterministic discrete events at non-deterministic times. The discrete event components of systems are called discrete event systems (DES). Communication networks, multiprocessor computer systems, and distributed data bases are examples of discrete event systems. In recent years, new systems have been designed with coordinating discrete event components. Examples are systems found in transportation, such as IVHS--intelligent vehicle and highway systems--as well as in manufacturing, aerospace, and in computer-based process-control systems. In this thesis we investigate formal methods applied to discrete event systems. Formal methods are used to model systems and to verify their correctness with respect to a set of properties. If a system is successfully verified to have a given attribute, no behavior or execution path of the system can ever be found to contradict this fact. Formal specification of a system consists of modeling it via a chosen paradigm such as FSM, Petri Nets, Process Algebras, or logics such as LTL, or CTL. Formal verification involves assertions about the behavior of the modeled system within some formal assertion context such as logic or formal languages. Formal methods range from general theorem proving to restricted logics and finite automata methods. In this thesis, we provide a background on formalisms based on finite automata, summarizing results in the area. A detailed discussion on L-automata follows, which explains how L-automata reduction and induction techniques are used to analyze large and complex discrete event systems. We report in this thesis our extensive experience in formally specifying and verifying discrete event components of a very large and complex system, namely the PATH control system, using the L-automata framework. Some systems combine discrete event system (DES) components with continuous variable dynamical system (CVDS) components. These systems are called hybrid systems. These systems are characterized by switching continuous variable dynamical laws according to discrete events. Although traditional systems theory can be used to analyze a hybrid system at a given switch position, new theories and methods are required in order to accurately model the combined DES and CDVS components. In this thesis, we also investigate formal methods for hybrid systems. A review of the developments which lead to hybrid system models is presented. The major contribution of this thesis is an automata-theoretic model of a class of hybrid systems, namely real-valued linear time invariant (LTI) hybrid systems. We show that there exist subclasses of LTI hybrid systems which can be treated exactly, thus allowing the proposed semi-decision analysis procedures, if they terminate, to establish whether a given hybrid system performs a given task. Also, we show that general real-valued LTI hybrid systems can be treated via proposed approximation methods.