In formal verification, a designer first constructs a model, with mathematically precise semantics, of the system under design, and performs extensive analysis with respect to correctness requirements. The appropriate mathematical model for embedded control systems is hybrid systems that combines the traditional state-machine based models for discrete control with classical differential-equations based models for continuously evolving physical activities. In this article, we briefly review selected existing approaches to formal verification of hybrid systems, along with directions for future research.  Categories and Subject Descriptors Verification. Hybrid systems, Control systems, Model checking, Formal methods Model-based design offers a promising approach for detecting and correcting errors in early stages of system design [33, 37, 49] . In this methodology, a designer first constructs a model, with mathematically precise semantics, of the system under design, and performs extensive analysis with respect to correctness requirements before generating the implementation from the model. Embedded systems, such as controllers in automotive, medical, and avionic systems, consist of a collection of interacting software modules reacting to a continuously evolving environment. The appropriate Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. EMSOFT'11, October 9-14, 2011, Taipei, Taiwan. Copyright 2011 mathematical model for design of embedded control systems is hybrid systems that combines the traditional models for discrete behavior with classical differential-and algebraicequations based models for dynamical systems. Such models can capture both the controller -the system under design, and the plant -the environment with continuously evolving physical activities in which the system operates. Given that (1) automated verification tools have recently been successful in finding bugs in "real-world" hardware protocols and device drivers [13, 15] , (2) tools such as Stateflow/Simulink are commonly used in automotive and avionics industry for modeling, and (3) high assurance is a necessity in safetycritical applications that deploy embedded software, formal verification of hybrid systems has been a vibrant research area for the past 20 years. This article is an overview of current research directions, aimed at providing an introductory "roadmap" rather than a comprehensive survey. In early 1990s, formal models for discrete reactive systems were integrated with models for dynamical systems [2, 41] . The model of hybrid automata [1, 2, 29] has emerged to be a popular choice. A hybrid automaton is an extended finitestate machine whose state consists of a mode that ranges over finitely many discrete values and a finite set of realvalued variables. Each mode is annotated with constraints that specify the continuous evolution of the system, and edges between modes are annotated with guards and updates that specify discrete transitions. For example, the behavior of a self-regulating thermostat can be described by a hybrid automaton with two modes, on and off, and a single real-valued variable T modeling the temperature. To specify how the temperature changes in the mode on, we can annotate the mode with a differential equation, say, T = k(70 − T ), for a constant parameter k. Alternatively, we can use a differential inequality, say, k 1 ≤Ṫ ≤ k2, for two constants k 1 and k2, to specify the dynamics approximately using only bounds on the derivative. Associating the mode on with an invariant constraint T ≤ 70 specifies that the system must exit this mode before the temperature exceeds 70. An edge from the mode on to the mode off with the guard T ≥ 68 specifies that, whenever the temperature exceeds 68, the system can discretely change its state by updating the mode to off. A hybrid automaton can naturally be interpreted as an infinite-state transition system, and this forms the basis for formalizing classical notions such 273 as safety verification, property-preserving abstractions, and simulation relations, for hybrid systems. The commercial modeling tools such as Stateflow/Simulink (see www.mathworks.com) and Modelica (see www.modelica. org) are routinely used in a wide range of industries. Conceptually, it should be possible to compile models expressed in such tools into formal notations such as hybrid automata. This has turned out to be difficult in practice due to the richness of features in commercial tools and the lack of a standardized formal semantics of such features (see [35] for efforts aimed at semantics-preserving transformations across modeling notations). In the safety verification problem for hybrid systems, we are given a hybrid systems model M , a set I of initial states of M , and a set S of "safe" states of M , and we want to check whether every execution of M starting in an initial state always stays within the set of safe states, and if not, report a violating execution as a counter-example. For instance, given the hybrid systems model of a collision avoidance protocol, we want to check whether the distance between two vehicles stays greater than the safety threshold for given initial conditions. Let us first note that the safety verification problem of hybrid systems cannot be solved algorithmically: with the exception of classes that severely restrict the allowed dynamics of real-valued variables such as timed automata [5] and initialized rectangular automata [32] , the safety verification problem is undecidable [1, 32] . Symbolic reachability algorithms for safety verification try to compute the set R of reachable states of a hybrid system M in an iterative manner starting from the set I of initial states. The algorithm checks, at every step of the iteration, if the current set R of reachable states is a subset of the set S of safe states, and if not, it terminates with a counter-example. In general, there is no termination guarantee, as the algorithm may keep adding more and more states to R without being able to deduce that the system is safe. The key challenge to efficient implementation is to identify a suitable representation for the set of states that supports the operations used by the iterative reachability computation. The tool HyTech was the first model checker to implement symbolic reachability analysis for hybrid systems [7, 31] . For a hybrid automaton with n real-valued variables, each reachable set is represented by associating a finite union of ndimensional polyhedra with each mode, where a polyhedron is represented as a conjunction of linear inequalities over variables. Such a polyhedra-based representation is appealing due to the use of polyhedra in many computing applications and the availability of open-source libraries for manipulating them (c.f. [12] ). The models are restricted to the class of linear hybrid automata (LHA): guards, updates, and invariants involve only linear expressions, and the dynamics is specified using differential inequalities that are linear constraints over first-order derivatives. For example, the LHA-admissible dynamicsẋ =ẏ ∧ 1 ≤ẋ ≤ 2 describes two-dimensional motion along the diagonal line with bounds on speed. For LHA, the polyhedral representation is closed under both discrete transitions corresponding to mode-switches and continuous evolution according to differential constraints in a mode: given a polyhedron R describing the set of current states, the set R of states that the system can reach after a discrete mode-switch to a mode m, is a polyhedron that can be computed effectively from R, and the set R of states that the system can reach as a result letting it evolve continuously according to the dynamics associated with the mode m, is also a polyhedron that can be computed effectively from R . The most commonly used dynamics in mathematical design of control systems involves linear differential equations: if x represents the vector of state variables, u represents the vector of input variables, a linear system is described by the equationẋ = Ax + Bu, where A and B are matrices of appropriate dimensions. Such dynamics is not allowed in LHA. Linear hybrid systems (LHS) refers to the class of hybrid automata where guards, updates, and invariants involve only linear expressions, and the dynamics is specified using linear differential equations. First note that the polyhedral representation is not closed under continuous evolution specified by linear differential equations: if x = 1 is the initial state and the dynamics is given by the linear differential equatioṅ x = x, the set of reachable states is the exponential curve given by e t , for real numbers t ≥ 0. Since manipulating transcendental functions is computationally difficult, a popular strategy, first advocated by the tool Checkmate [14], and later refined by the tool d/dt [11] , is to compute overapproximations of reachable sets using polyhedral representations. Given a polyhedron R representing the set of current states, to compute the set R of states that are reachable within a fixed time horizon Δ according to a given linear differential equation, the algorithm implements the following strategy. For every corner vertex v of R, it first computes the state v of the system at time Δ starting in state v. Then it computes the convex hull R 1 of all the corner vertices v of R and their respective images v . We are guaranteed that all the system trajectories start in the polyhedron R 1 and end in R 1 at time Δ, but are not necessarily inside R1 at intermediate times. The final step involves computing the polyhedron R 2 obtained by "face-lifting" R1: the number and normal vectors for facets of R 2 coincide with R1, but the facets are shifted outwards so as to include all reachable states upto time Δ. All these steps can be efficiently implemented for linear systems, and the resulting polyhedron R 2 is guaranteed to be a superset of the desired set R . The process can be repeated for successive time intervals, and the resulting approximation of the reachable set is called the flowpipe approximation. The complexity of operations on polyhedra is exponential in the number of dimensions (that is, the number of real-valued variables of the hybrid system), and since such operations are invoked repeatedly in symbolic analysis based on polyhedral representation, a significant body of work has been 274 aimed at battling this complexity and/or replacing polyhedra with alternative representations [11, 21, 36, 42] . Representation using zonotopes and support functions [22, 26] has so far resulted in the most scalable approach for the analysis of linear hybrid systems, leading to the tool SpaceEx that is able to analyze, for instance, a complex 28-dimensional helicopter controller [20] . In deductive verification, a designer interacts with a mechanized theorem prover to generate proofs of correctness of systems. For safety verification of discrete systems, a classical proof principle relies on the notion of inductive invariants: to show that all executions of a system M starting in an initial set I stay within a safe set S, we identify a state property ϕ such that (1) all initial states satisfy ϕ; (2) ϕ is a subset of the desired safety property S; and (3) the property ϕ is preserved locally across system transitions (that is, no transition of the system changes the value of ϕ from 1 to 0). In interactive verification, the user proposes a property ϕ, and the analysis tool checks if ϕ is an inductive invariant. The concept of inductive invariants for discrete systems has been generalized and adopted to continuous-time dynamical (and hybrid) systems. We will informally explain the first such notion, called barrier certificates [47, 48] . To show that a dynamical system M with dynamicsẋ = f (x) with initial set I satisfies a safety property S, we identify a function ψ from the states to reals such that (1) in all initial states, the value of ψ is nonnegative; (2) in all unsafe states (that is, states not in the safe set S), the value of ψ is negative; and (3) the Lie derivate of ψ with respect to the vector field f is positive on the boundary set (called the barrier) characterized by ψ(x) = 0. The first two conditions ensure that the barrier separates the initial states from the unsafe states, and the third condition ensures that system trajectories cannot escape the barrier from inside as at the barrier the flow field points inwards. Together, these conditions imply that ψ(x) ≥ 0 is an inductive invariant of the system. Typically, the desired function ψ is a polynomial function of the system variables. It is also worth noting that the barrier certificates are closely related to the notion of Lyapunov certificates for stability in classical control theory. The notion of differential invariants generalizes barrier certificates [44] : it relaxes the third condition, and also allows more general forms of logical assertions as potential invariants. Verification of safety properties based on identifying inductive invariants avoids the iterative calculation of reachable state sets and is not limited to linear systems. The tool KeYmaera offers support to prove correctness of hybrid systems using deductive verification [43, 44] . To check whether a given polynomial certificate satisfies all the conditions necessary for it to be a barrier certificate, the tool needs to perform symbolic differentiation, and calculations such as simplification and quantifier elimination, with formulas in the theory of reals with arithmetic operators. To fully automate deductive verification, such a tool needs to automatically generate candidates for inductive invariants, and this remains an active area of research (see [28, 50] for automatic generation of invariants by instantiating templates and [45] for generating invariants by fixpoint computation). An abstraction A of a model M is a "simplified" model obtained from M such that proving safety and temporal properties of A is a sufficient condition for proving the corresponding properties of M . Abstraction is an effective strategy for scalability of verification tools, provided there is a way to compute A from M in a tool-supported manner, and a way to refine the current abstraction A if it is not adequate to prove the desired properties. In the case of hybrid systems, the simplicity of the abstract model A can be of various forms: A can be discrete while M is continuous; A can have linear dynamics while M has non-linear dynamics; and A can be a linear model of dimensionality lower than that of M . There is an extensive literature on automatic abstraction of hybrid systems. We note three representative examples.
Verification of hybrid systems has been performed applying different techniques (see REF for a recent survey).
Formal verification of hybrid systems
EMSOFT '11
Computer Science