Hybrid Systems: Computation and Control

Frontmatter

SACRES: A Step Ahead in the Development of Critical Avionics Applications

Abstract

Basically, aircraft engines can be divided into a control embedded system and a controlled system with its environment. The behaviour of the controlled system is given a priori, while the control system still needs to be designed in a way guaranteeing the correct overall behaviour under all operational conditions depending on the flight domain. A large quantity of functions in control systems can be described by a formal system expressed in block diagrams and state-based representations. These representations can be translated to formal based tools relying on the synchronous languages Signal and Statecharts. SACRES is a tool set supporting the design of safety-critical embedded control systems. It integrates the tools and specification techniques Statemate, Sildex, and Timing Diagrams with tool components for automatic code generation, formal verification based on model checking techniques, and an innovative approach for automatic code validation for target code generated from DC+. Technical achievements are

• The main benefits of the SACRES approach are reduced risks for design errors and decreased design times and costs for the development of dependable (safety critical) embedded systems. SACRES is an attempt to avoid unpredictability (particularly that arising from late feedback from testing) associated with development of safety critical systems, through the use of the maximum degree of automation, especially in respect of code generation and verification.
• An outstanding property of SACRES is the combination of specification styles and specification tools being applied in practice with automatic tools to establish provable correctness with respect to required properties. Both dependability and productivity are increased by automatic code generation from high-level specifications such that the generated code can be validated against higher levels by rigorous proofs.
• These techniques allow traditional tests by sampling to be replaced by rigorous checking techniques which correspond to 100% coverage of test cases. In order to address a global innovative approach in the near future which match the whole software configuration, the SACRES tool set should be interfaced with asynchronous techniques matching the operating system development. This raises an open question in the software development future new process.

Philippe Baufreton

Approximating Hybrid System Dynamics for Analysis and Control

Abstract

The objective of this lecture is to survey and assess the state of the research on methods for approximating hybrid system dynamics. For all but the most trivial dynamic systems, approximations are necessary to make analysis and controller synthesis tractable. This is true for both continuous-state systems and discrete-state systems, and theories have been developed in both domains to justify and guide model simplification and approximation (although ad hoc engineering judgment remains the method of choice in most applications). For hybrid systems, decidability results indicate that approximations will always be necessary to solve analysis and controller synthesis problems for even the simplest systems. These results will be reviewed briefly as a motivation for the work on approximation methods.

We will then consider two principal types of approximations that have been explored in the literature. The first set of methods approximates general hybrid system dynamics with simpler hybrid models for which some computational tools exist, such as linear or timed automata. The second set of methods generates finite-state discretizations of the continuous dynamics in a hybrid system so that tools for discrete-state systems can be applied. In both cases, the literature will be reviewed and success with applications will be assessed. Strengths and limitations of each approach will be summarized, and the types of problems that can be solved using each approach will be identified. Some software packages for building and approximating hybrid system models will also be reviewed and examples will be presented.

The final part of the lecture will discuss prospects for the future, both in terms of a theory for approximating hybrid systems dynamics and tools for computer-aided analysis and controller synthesis. Open problems and directions for future work will be identified.

Bruce H. Krogh

High-Level Modeling and Analysis of an Air-Traffic Management System

Abstract

This talk describes progress in a current project on modeling and analyzing the TCAS II aircraft collision-avoidance system.

The state of the art in formal methods applied to air traffic management systems involves specifying software behavior in detail, using formalisms such as Statecharts. Although such methods are precise, they do not help much in understanding the systems intuitively; nor do they enable analysis of high-level global requirements, such as “Under condition A, the planes will not crash.”

To aid people in understanding such systems, and to enable such analysis, we advocate defining high-level mathematical models for the system, including not only the control software, but also the airplanes, sensors, and pilots—that is, high-level hybrid system models.

In a current demonstration project at MIT and Berkeley, we have defined abstract models for the key system components of the new TCAS II (version 7) system. These are based formally on the Hybrid I/O Automaton (HIOA) model [1]. We are using these models to formulate and prove theorems about the behavior of the system under particular assumptions. Our results are intended only as illustrations—the models provide a foundation for study of a wide range of properties of the system’s behavior. We hope that this project will help to produce improved validation methods for air-traffic management systems.

Nancy Lynch

Geometric Categories, O-Minimal Structures and Control

Abstract

The theory of subanalytic sets is an excellent tool in various analytic-geometric contexts, including geometric control theory. (See [1], for example.)

One can axiomatize the notion of “behaving like the category of subanalytic sets (in manifolds)” by introducing the notion of “analyticgeometric category”. (The category of subanalytic sets is the smallest analytic-geometric category.) The objects of such a category share many of the hereditary and geometric finiteness properties of subanalytic sets. Proofs of the more difficult results of this nature, like the Whitney-stratifiability of sets and maps in such a category, often involve the use of charts to reduce to the case of subsets of ℝⁿ. For subsets of ℝⁿ, the theory of o-minimal structures on the real field, an abstraction of the theory of semialgebraic sets, provides an elegant and efficient setting in which to work. (See [2] and [3].)

(Some reasonable sets—like {(x, x ^r): x > 0} for irrational r, {(x, e^x): x>0}, and {(x, Γ(x)): x > 0}—are not globally subanalytic in ℝ². Because there are o-minimal structures on the real fieald which include these sets “at infinity”among their objects)

In analogy with the semilinear, semialgebraic and subanalytic settings, one considers hybrid systems whose relevant data (guards, resets, flows and so on) all belong to some o-minimal structure. It can be shown, for example, that such hybrid systems admit finite bisimulations; see [4].

Chris Miller

Polyhedral Flows in Hybrid Automata

Abstract

A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete updates with differential constraints for capturing continuous flows. Formal verification of hybrid automata relies on symbolic fixpoint computation procedures that manipulate sets of states. These procedures can be implemented using boolean combinations of linear constraints over system variables, equivalently, using polyhedra, for the subclass of linear hybrid automata. In a linear hybrid automaton, the flow at each control mode is given by a rate polytope that constrains the allowed values of the first derivatives. The key property of such a flow is that, given a state-set described by a polyhedron, the set of states that can be reached as time elapses, is also a polyhedron. We call such a flow a polyhedral flow. In this paper, we study if we can generalize the syntax of linear hybrid automata for describing flows without sacrificing the polyhedral property. In particular, we consider flows described by origin-dependent rate polytopes, in which the allowed rates depend, not only on the current control mode, but also on the specific state at which the mode was entered. We establish that flows described by origin-dependent rate polytopes, in some special cases, are polyhedral.

Rajeev Alur, Sampath Kannan, Salvatore La Torre

As Soon as Possible: Time Optimal Control for Timed Automata

Abstract

In this work we tackle the following problem: given a timed automaton, and a target set F of configurations, restrict its transition relation in a systematic way so that from every state, the remaining behaviors reach F as soon as possible. This consists in extending the controller synthesis problem for timed automata, solved in [MPS95,AMPS98], to deal with quantitative properties of behaviors. The problem is formulated using the notion of a timed game automaton, and an optimal strategy is constructed as a fixed-point of an operator on the space of value functions defined on state-clock configurations.

Eugene Asarin, Oded Maler

Verification of Hybrid Systems via Mathematical Programming

Abstract

This paper proposes a novel approach to the verification of hybrid systems based on linear and mixed-integer linear programming. Models are described using the Mixed Logical Dynamical (MLD) formalism introduced in [5]. The proposed technique is demonstrated on a verification case study for an automotive suspension system.

Alberto Bemporad, Manfred Morari

Orthogonal Polyhedra: Representation and Computation

Abstract

In this paper we investigate orthogonal polyhedra, i.e. polyhedra which are finite unions of full-dimensional hyper-rectangles. We define representation schemes for these polyhedra based on their vertices, and show that these compact representation schemes are canonical for all (convex and non-convex) polyhedra in any dimension. We then develop efficient algorithms for membership, face-detection and Boolean operations for these representations.

Olivier Bournez, Oded Maler, Amir Pnueli

A Geometric Approach to Bisimulation and Verification of Hybrid Systems

Abstract

An approximate verification method for hybrid systems in which sets of the automaton are over-approximated, while leaving the vector fields intact, is presented. The method is based on a geometricallyinspired approach, using tangential and transversal foliations, to obtain bisimulations. Exterior differential systems provide a natural setting to obtain an analytical representation of the bisimulation, and to obtain the bisimulation under parallel composition. We define the symbolic execution theory and give applications to coordinated aircraft and robots.

Mireille Broucke

Verification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations

Abstract

This paper presents a computational technique for verifying properties of hybrid systems with arbitrary continuous dynamics. The approach is based on the computation of approximating automata, which are finite-state approximations to the (possibly infinite-state) discretetrace transition system for the hybrid system. The fundamental computation in the generation of approximating automata is the mapping of sets of continuous states to the boundaries of the location invariants. This mapping is computed by intersecting flow pipes, the sets of reachable states for continuous systems, with the invariant boundaries. Flow pipes are approximated by sequences of overlapping convex polygons. The paper presents an application of the computational procedure to a benchmark hybrid system, a batch evaporator.

Alongkrit Chutinan, Bruce H. Krogh

Path Planning and Flight Controller Scheduling for an Autonomous Helicopter

Abstract

In this article we investigate how to generate flight trajectories for an autonomous helicopter. The planning strategy that we propose reflects the controller architecture. It is reasonable to identify different flight modes such as take-off, cruise, turn and landing, which can be used to compose an entire flight path. Given a set of nominal waypoints we generate trajectories that interpolate close to these points. This path generation is done for two different cases, corresponding to two controllers that either govern position or velocity of the helicopter. Based on a given cost functional, the planner selects the optimal one among these multiple paths. This approach thus provide a systematic way for generating not only the flight path, but also a suitable switching strategy, i.e. when to switch between the different controllers.

M. Egerstedt, T. J. Koo, F. Hoffmann, S. Sastry

Reachability Analysis Using Polygonal Projections

Abstract

This paper presents Coho, a reachability analysis tool for systems modeled by non-linear, ordinary differential equations. Coho represents high-dimensional objects using projections onto planes corresponding to pairs of variables. This representation is compact and allows efficient algorithms from computational geometry to be exploited while also capturing dependencies in the behaviour of related variables. Reachability is performed by integration where methods from linear programming and linear systems theory are used to bound trajectories emanating from each face of the object. This paper has two contributions: first, we describe the implementation of Coho and, second, we present analysis results obtained by using Coho on several simple models.

Mark R. Greenstreet, Ian Mitchell

Scale-Independent Hysteresis Switching

Abstract

This paper introduces a new switching logic inspired by the hysteresis switching logic considered in [7,11]. The new logic also uses hysteresis to prevent chatter, but unlike its predecessor in [7,11], it is “scale-independent” as well. The logic is shown to have the requisite properties for adaptive control applications.

João P. Hespanha, A. Stephen Morse

Well-Posedness of a Class of Piecewise Linear Systems with No Jumps

Abstract

In this paper, a well-posedness (existence and uniqueness of solutions) problem of bimodal systems given by two linear systems is addressed, where the definition of solutions of Carathéodory is used. This problem is a basic problem in the study of well-posedness for discontinuous dynamical systems. We give here a complete answer to this problem. The obtained result shows that the well-posedness of bimodal systems can be characterized by two properties: the preservation property of the lexicographic inequality relation between the two regions specifying the two modes, and the smooth continuation property.

Jun-ichi Imura, Arjan van der Schaft

A New Class of Decidable Hybrid Systems

Abstract

One of the most important analysis problems of hybrid systems is the reachability problem. State of the art computational tools perform reachability computation for timed automata, multirate automata, and rectangular automata. In this paper, we extend the decidability frontier for classes of linear hybrid systems, which are introduced as hybrid systems with linear vector fields in each discrete location. This result is achieved by showing that any such hybrid system admits a finite bisimulation, and by providing an algorithm that computes it using decision methods from mathematical logic.

Gerardo Lafferriere, George J. Pappas, Sergio Yovine

Synthesis of Control Software in a Layered Architecture from Hybrid Automata

Abstract

This paper deals with the synthesis of control software for hybrid systems specified as hybrid automata. Instead of generating the software from scratch, the synthesis is based on a generic layered software architecture which supports both periodic and event-triggered computations. The use of the layered software architecture as the framework for implementing hybrid controllers is motivated in the paper.

An automatic code generator HA2LS (from Hybrid Automata to Layered Systems) is introduced. HA2LS reads a specification in terms of hybrid automata and generates intermediate code that can be processed by the tools provided by the layered architecture. The generated software provides a clean interface for a control engineer to plug in the control algorithms. With externally supplied control algorithms and IO procedures, the synthesis of executable hybrid controllers can be completed. The generated code can also be used for simulation purposes if it is generated from the specification of the complete system including the plant. The code generator HA2LS together with the software architecture substantially shorten the time to implement hybrid controllers from hybrid automata.

Man Lin

An Overview of Hybrid Simulation Phenomena and Their Support by Simulation Packages

Abstract

Hybrid systems combine continuous behavior evolution specified by differential equations with discontinuous changes specified by discrete event switching logic. Numerical simulation of continuous behavior and of discrete behavior is well understood. However, to facilitate simulation of mixed continuous/discrete systems a number of specific hybrid simulation issues must be addressed. This paper presents an overview of phenomena that emerge in simulation of hybrid systems, reported in previously published literature. They can be classified as (i) event handling, (ii) run-time equation processing, (iii) discontinuous state changes, (iv) event iteration, (v) comparing Dirac pulses, and (vi) chattering. Based on these phenomena, numerical simulation requires the implementation of specific hybrid simulation features. An evaluation of existing simulation packages with respect to these features is presented.

Pieter J. Mosterman

Building Hybrid Observers for Complex Dynamic Systems Using Model Abstractions

Abstract

Controllers for embedded dynamic systems require models with continuous behavior evolution and discrete configuration changes. These changes may cause fast continuous transients in state variables. Time scale and parameter abstractions simplify the analysis of these transients, causing discontinuities in the state variables. The two abstraction types have a very different impact on the analysis of system behavior. We have developed a systematic modeling approach that introduces formal semantics for behavior generation. This paper discusses the implementation of this scheme in a hybrid observer designed to track embedded system behavior. The resultant observer is based on piecewise simpler continuous models with mode transitions defined between them. Actual mode transitions in the system are provided by a digital controller and directly obtained from measuring physical variables.

Pieter J. Mosterman, Gautam Biswas

Integration of Analog and Discrete Synchronous Design

Abstract

The synchronous family of languages (Lustre, Esterel, Signal, Statecharts) provide a great deal of support for verifying a control program at the design and compilation stage. However, a common aspect of embedded systems is that significant properties of the system can not be verified by formally analysing the controller (software) on its own. To analyse the system one requires to state and document assumptions on the environment. Furthermore, proving timeliness properties necessitates justifying a sampling interval and relating the synchronous step to metric time. Support for these activities is generally missing from current formal methods tools.

In this paper we exploit simulation models — based on physical modelling of the environment — together with theorem proving, to prove properties of a closed loop system.We report on the work in progress on a case study provided by Saab Aerospace where deductive tools such as NP-Tools and simulation environments such as MATRIXx-SystemBuild are jointly used for verifying designs in Statecharts or programs in Lustre. The case study treats temperature and flow control in a climatic chamber.

Simin Nadjm-Tehrani

Reachability Analysis of a Class of Switched Continuous Systems by Integrating Rectangular Approximation and Rectangular Analysis

Abstract

The paper presents a concept for the reachability analysis of switched continuous systems in which switching only occurs when the continuous state trajectory crosses thresholds defined by a rectangular partitioning of the state space. It combines an existing approach for approximating such systems by rectangular automata with an existing reachability algorithm for this class of hybrid automata. Instead of creating a complete abstraction of the original system by a rectangular automaton first and then analyzing it, in the presented procedure the flow conditions of the visited locations are determinded on-the-fly during the course of the analysis. The algorithm is illustrated with the help of a simple physical example.

J. Preußig, O. Stursberg, S. Kowalewski

Refinement and Continuous Behaviour

Abstract

Refinement Calculus is a formal framework for the development of provably correct software. It is used by Action Systems, a predicate transformer based framework for constructing distributed and reactive systems. Recently, Action Systems were extended with a new action called the differential action. It allows the modelling of continuous behaviour, such that Action Systems may model hybrid systems. In this paper we investigate how the differential action fits into the refinement framework. As the main result we develop simple laws for proving a refinement step involving continuous behaviour within the Refinement Calculus.

Mauno Rönkkö, Kaisa Sere

Computing Controllers for Nonlinear Hybrid Systems

Abstract

We discuss a procedure for synthesizing controllers for safety specifications for hybrid systems. The procedure depends on the construction of the set of states of a continuous dynamical system that can be driven to a subset of the state space, avoiding another subset of the state space (the Reach-Avoid set). We present a new characterization of the Reach-Avoid set in terms of the solution of a pair of coupled Hamilton-Jacobi partial differential equations. We also discuss a computational algorithm for solving such partial differential equations and demonstrate its effectiveness on numerical examples.

Claire Tomlin, John Lygeros, Shankar Sastry

Stabilization of Orthogonal Piecewise Linear Systems: Robustness Analysis and Design

Abstract

In previous work the stabilization of Orthogonal Piecewise Linear (OPL) systems was considered and a simple design technique was outlined. In this paper the problems of robustness analysis and design for OPL systems are investigated. It is shown that, due to simplicity in the algebra involved, piecewise-linear Lyapunov functions offer considerable ease in addressing robustness. Assuming real structured parametric uncertainties in general affine linear state-space models, time-varying or state-dependent uncertainties as well as modeling errors can be taken into account, while retaining the same spirit in the design procedure. Bounds for the uncertain parameters can be easily found using linear programming and the computational complexity is kept low. These issues complete the OPL framework and confirm that it constitutes a simple design technique for addressing stability, performance and robustness while taking into account control limitations.

C. A. Yfoulis, A. Muir, P. E. Wellstead, N. B. O. L. Pettit

Backmatter