QUARTERLY PROGRESS REPORT CONTRACTOR: University of California at Berkeley AGREEMENT NUMBER: F33615-98-C-3614 CONTRACT PERIOD: 9/1/99 - 12/31/03 TITLE: Integrated Design and Analysis Tools for Software Based Control Systems REPORT PERIOD: 7/1/01 - 9/30/00 SPONSOR: Air Force Research Laboratory (AFRL) TECHNICAL POC: Ray Bortner REPORT PREPARED BY: Tom Henzinger (tah@eecs.berkeley.edu) 0. Executive Summary Our effort integrates three tasks: formal modeling and verification; embedded software design; and controller design and analysis. We made substantial progress in all three directions. Some of the highlights include: solution of the controller synthesis problem for rectangular hybrid systems, a compositional model and verification algorithms for probabilistic hybrid systems, progress on the embedded virtual machine (E-machine), a visual editor for modal models and hybrid systems, a Giotto compiler, and multi-modal control algorithms for constrained nonlinear systems. 1. Research Status Formal Modeling and Analysis ============================ Model Checking Based Control Algorithms for Infinite-state Systems ------------------------------------------------------------------ A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories: Class 1 consists of infinite-state structures for which all safety and reachability games can be solved. Class 2 consists of infinite-state structures for which all omega-regular games can be solved. Class 3 consists of infinite-state structures for which all nested positive boolean combinations of omega-regular games can be solved. Class 4 consists of infinite-state structures for which all nested boolean combinations of omega-regular games can be solved. We give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies ("controller synthesis") for infinite-state games with arbitrary omega-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems. This result won a best paper award at CONCUR 2001 [8]. Compositional Modeling, Verification, and Control of Probabilistic Systems -------------------------------------------------------------------------- We present a compositional trace-based model for probabilistic hybrid systems [7]. The behavior of a system with probabilistic choice is a stochastic process, namely, a probability distribution on traces, or "bundle." Consequently, the semantics of a system with both nondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Refinement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semantics by introducing two scoping mechanisms. The first mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions. We give an algorithm for refinement checking based on simulation relations between probabilistic systems. Control Using Synchronous Software Systems ------------------------------------------ A controller is an environment for a system that achieves a particular control objective by providing inputs to the system without constraining the choices of the system. For synchronous systems, where system and controller make simultaneous and interdependent choices, the notion that a controller must not constrain the choices of the system can be formalized by type systems for composability. In a previous paper, we solved the control problem for static and dynamic types: a static type is a dependency relation between inputs and outputs, and composition is well-typed if it does not introduce cyclic dependencies; a dynamic type is a set of static types, one for each state. Static and dynamic types, however, cannot capture many important digital circuits, such as gated clocks, bidirectional buses, and random-access memory. We therefore introduce more general type systems, so-called dependent and bidirectional types, for modeling these situations, and we solve the corresponding control problems [6]. In a system with a dependent type, the dependencies between inputs and outputs are determined gradually through a game of the system against the controller. In a system with a bidirectional type, also the distinction between inputs and outputs is resolved dynamically by such a game. The game proceeds in several rounds. In each round the system and the controller choose to update some variables dependent on variables that have already been updated. The solution of the control problem for dependent and bidirectional types is based on algorithms for solving these games. Giotto ------ We have continued development on the time-triggered Giotto model of computation. Specifically, Christoph Kirsch, Arkadeb Ghosal, and Slobodan Matic built a Giotto compiler and run-time system based on the E-Machine (see below). The compiler can be tested under Linux: www.eecs.berkeley.edu/~fresco/giotto and has already been adopted by two courses on hard real-time software development (in Kiel, Germany, and Zurich, Switzerland). Ben Horowitz is currently implementing annotation validity checks, which check if a given set of Giotto constraints is consistent with a given platform (hardware and scheduler). Christoph is working on a distributed Giotto implementation. Arkadeb and Slobodan are implementing a dynamic link capability in Giotto. This will allow us to change control code at run-time. Embedded Software Design ======================== E-Machine --------- Christoph Kirsch and Tom Henzinger have been actively improving their embedded virtual machine (E-machine). The E-machine can be thought of as a facade for real-time operating systems (RTOSs). The goal is to separate the interaction between tasks and the environment from task computation and communication, such that a set of tasks behaves the same under all E-machine compatible RTOSs. In particular, timing requirements come from the physical environment and the application. In the more common approach, timing properties emerge as a result of the resources granted to a specific piece of computation. The main contributions of the E-machine model are a component architecture (tasks, drivers, and ports) and an interrupt (trigger) management mechanism. The distinction between tasks and drivers, the mutual exclusion of task ports, the restrictions that data transfer can only be achieved by drivers, and the run-time protection of task ports, implement a split-phase execution, which separates communication from computation and eases resource management. By enforcing the port accessibility and RTOS callbacks, it can effectively avoid priority inversion problems in preemptive execution. The defined instruction primitives are a set of operations for starting and stopping component computation and communication. These operations are typically triggered by external events, rather than task execution times. This abstraction makes data and time dependencies among tasks orthogonal to real-time scheduling algorithms. Interrupt handling is separated from tasks and underlying scheduling algorithms. This allows the E-machine architecture to support both time-triggered and event-triggered models. The abstraction provided by the E-machine is simple yet powerful. By restricting what kind of input can trigger the E-machine, and by providing patterns for designing drivers, different programming models can be supported. Distributed Embedded Machine on Real-Time CORBA ----------------------------------------------- Jie Liu has developed a strategy for realizing an implementation of Tom Henzinger and Christoph Kirch's embedded virtual machine (E-machine) on top of real-time CORBA, using its event service (as in the Boeing open control platform (OCP)). His extension to the E-machine is called the distributed E-machine architecture (DEMA). It intends to keep the computation and communication semantics of the E-machine while providing location transparency and prioritized event dispatching semantics in distributed systems, as implemented in the current OCP. The facilities of DEMA will be rich enough to support many programming models for real-time embedded systems, for example, hierarchical preemptive multitasking (HPM), time-triggered architectures (like Giotto), functional reactive programming (FRP and Timber), and the current OCP Controls API. It will ease the code generation process for (at least) the above programming models. The semantics of DEMA needs to be clean enough to support the publish/subscribe model of data distribution and precise mode switching across system tasks. Ideally, it will support hierarchical compositions of multiple run-time models. The execution of DEMA needs to be efficient enough to make it usable in hard-real time applications, e.g. UAV controllers and multiple UVA coordination. The main idea behind DEMA is to coordinate distributed E-machine activities through publish-and-subscribe. Since the E-machine can only be activated by triggers, the core of DEMA is to approperately distribute triggers. A simple way to coordinate E-machines is to view event channels as part of the environment, which is out of the scope of the E-machine. So, E-machines in this framework are independent. Independent E-machines fully comply to the "plug and play" philosophy of event channel models. But at the same time, by treating event notification as random events, we may lose some analyzability. Since we know event channel performance and the priorities of event dispatching, it is possible to take this knowledge into account when generating E-machine code. Time-Triggered Models --------------------- Jie Liu has been investigating the implications of realizing an E-machine on a time-triggered architecture (TTA). In an E-machine on TTA, only clocks trigger the execution of tasks. Tasks implement computation, and drivers implement communication. The resulting E-machine code is highly structured. Hierarchical Priority-Driven Multitasking ----------------------------------------- Jie Liu has also investigated realization of the hierarchical priority-driven multitasking model (HPM), which has been previously reported, on the E-machine. Unlike TTA, the HPM model is an event-triggered model. Computation and communication can be triggered by irregular events. But like TTA, tasks produce their outputs at predefined time instants after they are triggered. In this model, tasks have priorities, WCETs, and deadlines. Whenever a task is triggered, it is handed over to the RTOS scheduler to be executed. Tasks are granted at least their requested WCET before their deadlines. The output are only produced when the deadline is reached, so we obtain time determinacy. Precise Mode Switching ---------------------- Both TTA and HPM models above support precise mode switching. A mode switch is a reconfigurations of the system. It is triggered by mode-switching events. Precise mode switching means that whenever a mode switch happens, no tasks is running, and the system is in a quiescent state. Precise mode switching can be handled at the E-machine level, where we use the disable and the terminate instructions. For example, the mode-switching event can trigger a block of E-machine code, inside of which, the E-machine can conditionally disable future triggers and terminate unfinished tasks, cooperatively or non-cooperatively. Visual Syntaxes --------------- We have made a number of architectural improvements to the user interface infrastructure in Ptolemy II, with an eye towards making it easier to create useful modal models and hybrid systems. These changes include restructuring the basic UI classes so that extending and customizing it to a domain-specific context is easier. Among the changes, for example, is a mechanism by which a visual element, such as an icon representing an actor or a state, can have a customized interaction with the designer, for example to create domain-specific ways of customizing the parameters of a component. We have also made a number of improvements to the finite-state-machine editor, making it easier to define interesting hybrid systems. Finally, we have created a visual editor for modal models that makes it very easy to construct one. This editor hierarchically combines finite state machines with models in any other domain. Using the continuous-time domain, one gets hybrid systems. Controller Design and Analysis ============================== Multi-Modal Control of Constrained Nonlinear Systems ---------------------------------------------------- T. John Koo, George Pappas (University of Pennsylvania), and Shankar Sastry presented a formal approach of hybrid system design for multi-modal control. In multi-modal control paradigm, a set of controllers of satisfactory performance have already been designed and must be used. Each controller may be designed for a different set of outputs in order to meet the given performance objectives and system constraints. When such a collection of control modes is available, an important problem is to be able to accomplish a variety of high level tasks by appropriately switching between the low-level control modes. They proposed a framework for determining the sequence of control modes that would satisfy reachability tasks. The proposed framework exploits the structure of output tracking controllers in order to extract a finite graph where the mode switching problem can be efficiently solved, and then implement it using the continuous controllers. Special emphasis is put on scalability and interoperability to cover the complete design flow from control law derivation, and mode switching synthesis to architecture conception. Throughout, a helicopter based unmanned aerial vehicle is used as a design example to demonstrate the effectiveness of the proposed design paradigm for solving the multi-modal control problem. Hierarchical System Architecture For Single-Agent Multi-Modal Systems --------------------------------------------------------------------- T. John Koo and Shankar Sastry presented a hierarchical system architecture for single-agent multi-modal systems. The layered system is designed to promote proof obligations so that system specification at one level of granularity conforms with that at another level and vice versa. The design principle for the construction of the hierarchy is based on bisimulation with respect to reachability specifications. Therefore, a higher-level system and a lower-level system are bisimilar. The approach is illustrated by designing a system architecture for controlling an autonomous agent. Hardware-in-the-loop Simulation of Multi-Vehicle Multi-Modal Embedded Systems ----------------------------------------------------------------------------- To design embedded systems for the control of autonomous vehicles for collectively delivering high levels of mission reliability has been putting tremendous pressure on control and software designers in industry. Hardware-in-the-loop (HIL) simulation allows testing an embedded computing device by replacing the real-world environment at the device's input-output interface with a simulated environment. HIL simulation is particularly effective when normal testing is dangerous or costly. HIL simulation facilitates {\em repeatable} testing, as well as quantification of design tradeoffs. T. John Koo, Benjamin Horowitz, Judy Liebman, Cedric Ma, Ron Tal, Tom Henzinger, and Shankar Sastry started to look into the issues on the design of a HIL simulation system for a group of unmanned aerial vehicles (UAVs). 2. Interactions and Technology Transfer Interactions ------------ * Jie Liu attended working group meeting at Boeing in St. Louis in August, and presented a talk entititled "Integrating E-Machine Concepts with Open Control Platform." He also early to work with Brian Mendel of Boeing on realizing an implementation of Tom Henzinger and Christoph Kirch's embedded virtual machine on top of the OCP. * Christoph Kirsch also attended the working group meeting at Boeing in St. Louis in August, and presented a description of the E-machine concept. * Zoltan Kemenczy and Sean Simmons of Research in Motion, Ltd., Waterloo, Canada, have contributed a Matlab interface package for Ptolemy II. This interface includes a C++ Java Native Interface translation layer, a ptolemy.matlab.Engine java class, and a ptolemy.matlab.Expression actor class that is similar in nature to ptolemy.actor.lib.Expression. The Matlab expression actor allows users to define the functionality of an actor in Matlab. * Aleksandar Necakov, also of Research in Motion Limited, has contributed a data-polymorphic version of the IIR (infinite impulse response) filter actor. * With the beginning of the semester, we have started an embedded software seminar series. Topics so far have included: -- Rupak Majumdar, "Symbolic algorithms for infinite-state systems" -- Jie Liu, "Hybrid System Modeling in Ptolemy II" -- Anton Cervin (Lund), "Analysis and Simulation of Control Loop Timing" * Also with the beginning of the semester, we have restarted our weekly study group. Topics so far include: -- F. Thoen, M. Cornero, G. Goossens, and H. De Man, "Software Synthesis for Real-Time Information Processing Systems." * Anton Cervin, a control engineering researcher from Lund, Sweden, visited our group for four weeks. * Tom Henzinger gave a Cray Distinguished Lecture on hybrid systems at the University of Minnesota (Minneapolis, Minnesota) on September 24. * Tom Henzinger and Christoph Kirsch presented the E machine at Honeywell Technology Labs on September 25. Technology Transfer ------------------- * Giotto, the compiler and run-time system developed at Berkeley, are being used in courses on hard real-time system development in Kiel, Germany, and Zurich, Switzerland. See http://www.aut.ee.ethz.ch/~sanvido/JGiotto/ and http://www.informatik.uni-kiel.de/inf/von-Hanxleden/teaching/WS2001-02/Mindstorms_Praktikum/index.html. * Giotto tools are currently being evaluated by Audi in Ingolstadt, Germany (where Tom Henzinger and Christoph Kirsch gave a presentation on September 13 via video conference, because all flights were grounded) and by TTTech in Vienna, Austria (where Christoph Kirsch will visit in November) for possible adoption. Personnel --------- No changes. 4. Publications [1] Edward A. Lee, "Soft Walls - Modifying Flight Control Systems to Limit the Flight Space of Commercial Aircraft," Technical Memorandum UCB/ERL M001/31, University of California, Berkeley, CA 94720, September 15, 2001. [2] Edward A. Lee, "Embedded Software," Technical Memorandum UCB/ERL M01/26, University of California, Berkeley, CA 94720, July 12, 2001. (joint work with Mobies) [3] Xiaojun Liu, Yuhong Xiong, and Edward A. Lee, "The Ptolemy II Framework for Visual Languages," poster paper, Symposium on Visual Languages and Formal Methods, Stresa, Italy, Sept. 5-7, 2001. (joint with Mobies). [4] T. J. Koo, S. Sastry, "Bisimulation Based Hierarchical System Architecture for Single-Agent Multi-Modal Systems," submitted to Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Springer-Verlag, 2002. [5] T. J. Koo, G. J. Pappas, and S. Sastry, "Multi-Modal Control of Constrained Nonlinear Systems Software-Enabled Control: Information Technology for Dynamical Systems," Tariq Samad and Gary Balas (Eds.), IEEE Press, 2002 [6] Luca de Alfaro, Thomas A. Henzinger, and F.Y.C. Mang. The control of synchronous systems, part II. Proceedings of the 12th International Conference on Concurrency Theory (CONCUR 2001), Lecture Notes in Computer Science, Springer-Verlag, 2001. [7] Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. Proceedings of the 12th International Conference on Concurrency Theory (CONCUR 2001), Lecture Notes in Computer Science, Springer-Verlag, 2001. [8] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Symbolic algorithms for infinite-state games. Proceedings of the 12th International Conference on Concurrency Theory (CONCUR 2001), Lecture Notes in Computer Science, Springer-Verlag, 2001. Best paper award. 5. Financial Data Provided separately on a quarterly basis by the university.