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: 4/1/01 - 6/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: the flight control software of a UAV rotorcraft has been implemented in Giotto (at ETH Zurich in collaboration with UC Berkeley); a virtual embedded machine for portable, mobile real-time code has been defined; exact and blended mode switching mechanisms have been implemented and studied in Ptolemy; hierarchical, multi-modal control and software architectures have been proposed and analyzed for derivability and predictability. 1. Research Status Formal Modeling and Analysis ============================ Giotto ------ We continued development on the time-triggered Giotto model of computation. Specifically, we are investigating the schedulability of Giotto on distributed platforms (Ben Horowitz) and we have implemented a Giotto compiler on a UAV rotorcraft from ETH Zurich (Christoph Kirsch, and Marco Sanvido drom ETH). All ground tests of Giotto on the model helicopter have been successfully completed and we are currently awaiting some sort of certification for flying. Giotto implements the glue (scheduling) code for the entire flight control systems, which manages the execution of native software tasks written in Oberon. The first Giotto paper got published at the June 2001 ACM Workshop for Languages, Compilers, and Tools for Embedded Systems: Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. Dynamic Programming Algorithms for Controller Synthesis ------------------------------------------------------- Symbolic model checking algorithms for system verification can be viewed as dynamic programs. We showed that the same dynamic programming schemes can also be used for the automatic synthesis of optimal control strategies. This work lies the foundation for using a model-checking tool such as HyTech for controller synthesis. We published these results at the June 2001 IEEE Symposium on Logic in Computer Science. Dynamic programs, or fixpoint iteration schemes, are useful for solving many problems on state spaces, including model checking on Kripke structures ("verification"), computing shortest paths on weighted graphs ("optimization"), computing the value of games played on game graphs ("control"). For Kripke structures, a rich fixpoint theory is available in the form of the mu-calculus. Yet few connections have been made between different interpretations of fixpoint algorithms. We study the question of when a particular fixpoint iteration scheme f for verifying an omega-regular property L on a Kripke structure can be used also for solving a two-player game on a game graph with winning objective L. We provide a sufficient and necessary criterion for the answer to be affirmative in the form of an extremal-model theorem for games: under a game interpretation, the dynamic program f solves the game with objective L if and only if both (1) under an existential interpretation on Kripke structures, f is equivalent to EL, and (2) under a universal interpretation on Kripke structures, f is equivalent to AL. In other words, f is correct on all two-player game graphs iff it is correct on all extremal game graphs, where one or the other player has no choice of moves. The theorem generalizes to quantitative interpretations, where it connects two-player games with costs to weighted graphs. While the standard translations from omega-regular properties to the mu-calculus violate (1) or (2), we give a translation that satisfies both conditions. Our construction, therefore, yields fixpoint iteration schemes that can be uniformly applied on Kripke structures, weighted graphs, game graphs, and game graphs with costs, in order to meet or optimize a given omega-regular objective. Embedded Software Design ======================== E-Machine --------- We have initiated an effort to define a "virtual machine" layer that abstracts the real-time and task interaction properties of an embedded system. The intent of the virtual machine is to serve as a target for a problem-oriented "controls API," and to be implementable on a variety of hardware/software architectures, including the current Boeing OCP. The virtual machine layer concept is our proposal to reconcile the needs of distributed supervisory control, which matches a publish and subscribe style of interaction using real-time CORBA, with lower-level hard-real-time control, which matches time-driven models such as FRP (from Yale) and Giotto (from Berkeley). At the same time, the virtual machine is attempting to address issues of concurrency management, particularly with respect to precise reactions and precise mode switching, in a way that is independent of the level of control being applied. Thus, the same conceptual framework can be shared. A first attempt at this virtual machine definition has been carried out by Christoph Kirsch and Tom Henzinger, and is described at: http://www.eecs.berkeley.edu/~fresco/giotto/refs Their virtual machine is called the E-machine, for "embedded machine." A program in this virtual machine consists of sets of tasks that take time and cannot be logically interrupted. There are no synchronization points between these tasks, thus avoiding a key source of problems with deadlock and unexpected nondeterminacy in concurrent programs. Instead, interactions between tasks are through ports. Input ports provide values that do not change during execution of the task. Output ports are updated only at the completion of the task. This is key to the operation of the virtual machine, and provides the principle mechanism for achieving predictable behavior. Tasks take time to execute, and execute concurrently with other tasks. The virtual machine does not define the underlying task scheduling model. That scheduling model would typically be provided by an underlying real-time OS. A dispatcher enables tasks for execution, and runs at the highest priority. The only assumption made about the underlying task scheduling model is that if the dispatcher has work to do, then it will execute, preempting all other tasks. In addition to tasks that take time, the virtual machine defines "drivers," which are tasks that conceptually execute instantaneously. These execute at the priority of the dispatcher. Time information is provided by the environment through ports, and these ports can trigger the enabling of tasks. Ports can also be used to signal the completion of a task, and activation of tasks can depend on port values. An E machine is an interpreter for E code. A compiler could generate the E machine interpreter, including the task manager (RTOS generation). Jie Liu has developed a proposal for a distributed E machine interpreter built using the Boeing OCP. This is an evolving proposal, and discussions with Boeing are under way. Virtual Machine Working Group ----------------------------- On June 13, we held an all day meeting at Berkeley to get inputs from the technology developers in SEC on the virtual machine concept. Attending were: John Peterson, Yale Richard Kieburtz, OGI Jie Liu, Berkeley Walid Taha, Yale Johan Nordlander, OGI Tom Henzinger, Berkeley Edward A. Lee, Berkeley Ben Horowitz, Berkeley Magnus Carlsson, OGI Joern Janneck, Berkeley Xiaojun Liu, Berkeley Jie Liu gave an overview of the OCP, and we discussed a virtual machine interpretation of the OCP. Johan Nordlander described the object model underlying O'Haskell (now called Timber), which we identified as a programming model rather than a virtual machine. Magnus Carlsson described an alternative to the OCP event channel for task interaction. Tom Henzinger described his strawman virtual-machine design, and argued that it offers to the virtual machine concept several key ideas: - atomic execution ("drivers") - ability to have a distributed time model. - Determinism in two dimensions: + Time it takes to do something (delay committing results) + Values of inputs and outputs (double buffering) Jie Liu described our hierarchical preemptive multitasking (HPM) domain in Ptolemy II, and we identified a realization of this domain on the strawman virtual machine. This domain offers a solution to the precise mode change problem in the OCP, and shares with the E-machine the split phase read/commit of inputs and outputs. John Peterson described FRP, which he identified as low-level semantics work. FRP adds time flow to any existing language. It is possible that FRP could be used to represent the semantics of the virtual machine. Walid Taha described real-time FRP, an abstract subset on FRP with guaranteed bounds on execution time and space. We identified the following action items: - Sell the split phase execution concept. + Solves the precise mode change problem. + Introduces a measure of determinism. - Define the embedded machine + With a better syntax + Top-level control loop + An informal operational semantics + Define the task model + Type system (not in the critical path) + Distribution model (& connection to event channel model) + Prototype implementation - Show how InputDataAvailable() can be converted to a split phase execution. + Backward compatible version might assume this is a driver. - Show have various programming models map onto the EM. + Concurrent real-time FRP + HPM (hierarchical preemptive multitasking) + Giotto + Priority-driven publish/subscribe + Timber + Rate monotonic scheduling Blending Controllers -------------------- Linda Wills and Bonnie Heck of Georgia Tech have been working on "blending controllers," where during a mode change, the control laws of two controllers are blended in a controlled way during the transition between the two controllers. These are modal (hybrid) controllers where instead of abruptly switching from one control law to another, an intermediate "blending" mode is use to gradually turn over control from one to the other. We began working with them on exploring ways of realizing these controllers, first via conference calls, and then when Linda Wills and Murat Guller visited us on 6/5/01 and 6/6/01. They posed the question of how to identify a suitable programmer's model for such modal controllers. We explored various alternatives, including mechanisms that could be built immediately in Ptolemy II, but found none of them suitable. We then discovered that a small change to the FSM (finite state machine) domain in Ptolemy II would enable a very clean programmer's model. In this model, a three state FSM is defined where in the first state, controller A is active and in the third state, controller B is active. In the second state, both controllers are active and their outputs are blended using an expression. The small change required in the FSM domain is that states must be able to have more than one active refinement. This turned out to be relatively easily to implement. Xiaojun Liu and Jie Liu completed an implementation in about one hour, and we constructed a simple demonstration system in about another half hour. We have set up access at Georgia Tech to our CVS tree so that we can continue to collaborate on this code development. Generalized Modal Models ------------------------ An outcome of the meeting with Georgia Tech (see above) was the realization that the Ptolemy II notion of a modal controller can be usefully generalized to one where a mode can have more than one (concurrent) refinement. The finite-state machine governing the mode changes can then be viewed as providing a mask, making some subset of the actors of a model visible to the director. This appears to be a significant increase in expressiveness over our prior *-charts formalism, which is a generalization of Statecharts and hybrid systems. Some possible applications of this formalism: 1) It could be used for managing redundant systems and doing fault detection and isolation. 2) It could be that heterochronous dataflow is a special case. 3) It could be viewed as a structured mutations approach. Xiaojun Liu is exploring this concept further. HPM (formerly RTOS) Domain -------------------------- Jie Liu has made major progress on his model of computation supporting precise reactions in the context of preemptive multitasking. In the previous reporting period, we reported a Ptolemy II domain called the RTOS domain that modeled RTOS-style preemptive multitasking. Jie has elaborated the semantics of this domain in very interesting ways, and has come up with a new model of computation that is significantly different from the previous version. We are calling this domain the HPM domain, for hierarchical preemptive multitasking. The key idea in HPM is that of split-phase firing, inspired by the Giotto model. In this manifestation, actors read and locally cache input data when their prefire() method is invoked, and (optionally) begin computation in a background process that executes concurrently with other processes with some specified priority. Not until the fire() method is invoked, however, do these actors write output data. In Jie's model, the actors declare their execution time, and the fire() method is invoked after they have had available CPU execution time equal to this declared value. A dispatcher process keeps track of invocations of actors with higher priority so that the process is assured of getting the declared CPU time. Since the outputs are not committed until that time has elapsed, there are several possible design patterns that can be overlayed on this: * Terminator pattern. If a process is not ready to produce outputs when its time has elapsed, then it has violated its contract on declared execution time, and it is terminated, not to be invoked again. * Anytime pattern. If a process has not completed its computation when its time has elapsed, then partial results are extracted and produced. * Laisez faire pattern. When the fire() method is invoked, it performs a join with the executing process, allowing it to run to completion. There are circumstances where each of these patterns is appropriate, and the choice depends on the application. It does not make sense to fix one of these choices in the modeling framework. Continuous-Time Domain ---------------------- With the help of Gautam Biswas and others at Vanderbilt University, Jie Liu identified limitations in the semantics of the CT domain (continuous time) when combined with finite state machines (FSMs) to make hybrid systems. Previously, actors were identified as either discrete or continuous, and the CT kernel treated the two differently. Any actor downstream from a discrete actor was also discrete. However, when building hybrid systems, it is common for an actor to interact with both discrete and continuous signals. Jie solved the problem by identifying signals instead of actors as discrete or continuous, and using a mechanism similar to type resolution to determine for each signal whether it is discrete or continuous. Jie describes his solution: "The solution is somewhat like a type system. In particular, it deals with signal types. For example, an integrator has input type CONTINUOUS and output type CONTINUOUS; a sequence actor has input type DISCRETE and output type DISCRETE; an event generator has input type CONTINUOUS and output type DISCRETE; a waveform generator has input type DISCRETE and output type CONTINUOUS, and so on. For domain polymorphic actors, their output type are constrained to be the same as their input type. (In a sense, there are only equalities in this type system). The signal type of a port can be set manually by adding a parameter "signalType", with value "CONTINUOUS" or "DISCTETE", to the port. All the ports of a CTCompositeActor, which is the container for hybrid systems, are by default CONTINUOUS. But users can force one or more ports to be DISCRETE by adding the parameter. The CTScheduler will check whether all the ports has a fixed type which does not conflict with all of it connections. And then partition the topology into a continuous cluster and a discrete cluster. The discrete cluster is only executed between iterations of continuous time execution. I have added another demo called Switch to illustrate this feature. A discrete event source triggers a hybrid system to switch between a sine wave and a constant. The demo is listed under CT domain in the quick tour." Controller Design and Analysis ============================== High Confidence Control of Multi-Modal Systems ---------------------------------------------- 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. T. John Koo, George Pappas (University of Pennsylvania), and Shankar Sastry presented a framework for determining the sequence of control modes that will satisfy reachability tasks. Our 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. Our approach is illustrated on a robot manipulator example, where we determine the mode switching logic that achieves the given reachability task. Hierarchical System Architecture for Multi-Agent Multi-Modal Systems ------------------------------------------------------------------ T. John Koo presented a hierarchical system architecture for multi-agent multi-modal systems. The design principle for the construction of the hierarchy is based on bisimulation and therefore a higher-level system and a lower-level system are bisimilar. The layered system is designed to promote proof obligations so that system specification at one level of granularity conforms with system specification at another level and vice versa. The approach is illustrated on designing a system architecture for executing a mission of controlling a group of autonomous agents in the pursuit of multiple evaders. Hierarchical Approach for Design of Multi-Vehicle Multi-Modal Embedded Software ------------------------------------------------------------------------------- Embedded systems composed of hardware and software components are designed to interact with a physical environment in real-time in order to fulfill control objectives and system specifications. T. John Koo, Judy Liebman, Cedric Ma, and S. Shankar Sastry addressed the complex design challenges in embedded software by focusing on predictive and systematic hierarchical design methodologies which promoted system verification and validation. First, they advocate a mix of top-down, hierarchical design and bottom-up, component-based design for complex control systems. Second, it is their point of view that at the level closest to the environment under control, the embedded software needs to be time-triggered for guaranteed safety; at the higher levels, we advocate an asynchronous hybrid controller design. We briefly illustrate our approach through an embedded software design for the control of a group of autonomous vehicles. 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). Decidable and Semi-decidable Controller Synthesis for Classes of Discrete ------------------------------------------------------------------------- Time Hybrid Systems ------------------- Rene Vidal, Shawn Schaffert, Omid Shakernia, John Lygeros, Shankar Sastry presented classes of discrete time hybrid systems for which the classical algorithm for computing the maximal controlled invariant set and the least restrictive controller is computable and guaranteed to terminate in a finite number of iterations. We show how the algorithm can be encoded using quantifier elimination, which leads to a semi-decidability result for definable hybrid systems. For discrete time linear systems with linear constraints that are either controllable or nilpotent and have bounded disturbances, we show that the controlled invariance algorithm terminates in a number of iterations which is at most the dimension of the system. Both in the hybrid and in the linear case, our results are much more general than the corresponding ones for continuous time systems. Finally they show that for linear systems with ellipsoidal constraints, an approximated solution can be obtained using robust convex programming. They provide an example showing that our algorithm gives better estimations than other ellipsoidal methods and is more efficient than the exact method for linear constraints. 2. Interactions and Technology Transfer Interactions ------------ * Weekly SEC meetings, Wednesdays 3-4pm. Topics that were covered include: - Marco Sanvido from ETH Zurich gave a presentation on "Autonomous Flying Model Helicopter Research at the Federal Institute of Technology, Zurich" on 4/12/01. - David Statezni from Rockwell Collins gave a presentation on their SEC project on 4/18/2001. - Tom Henzinger on A Theory of Component Interfaces, describing joint work with Luca de Alfaro and Freddy Mang on 4/25/01. - Christoph Kirsch and Jie Liu on synergies and distinctions between the E-machine specification and the RTOS domain, on 5/16/2001. * We had an extensive dialog with Brian Mendel and others at Boeing on the role of the Ptolemy project in the OCP and the possible solutions to the precise mode change problem. This dialog took the form of a working document on OCP/Ptolemy Integration passed back and forth. * Christoph Kirsch completed his embedded software course, where there were the following pertinent final project presentations: - Alvin AuYoung, Daniel Yoo: Tutebot: An E-Machine Implementation - Carlo Cloet, Jeff Ustin: An Example of Synchronous Computation - Paul Griffiths, Jason Souder: Scheduled Computation through Re-entrant Interrupts - Elaine Cheong, Steve Neuendorffer: Ptolemy & Embedded Code Generation - Benjamin Horowitz, Shawn Shaffert: The Time-Triggered Machine * Sonia Sachs spent quite a bit of time with David Statezni and Carlos Netto from Rockwell, who are in the SEC program. She explained Ptolemy to them and showed them demos, particularly the ones that combines FSM, CT and DE. * Marius Minea tutored David Statezni and Carlos Netto on HyTech, which they are using in their SEC project. * On May 16, we gave an overview of our SEC project Ruzena Bajcsy, from NSF. * We collaborated with Georgia Tech to implement blending controllers in Ptolemy II (see above). * Organized the virtual machine working group meeting at Berkeley (see above). * We had extensive dialogs with Gautam Biswas and others at Vanderbilt University about realizing Hybrid Bond Graphs in Ptolemy. The Vanderbilt team has been helpful in working through problems with the software. * Joern Janneck and Johan Eker visited Paul Hudak and John Peterson at Yale to discuss collaboration between the Ptolemy effort and the FRP (functional reactive programming) effort. This visit significantly improved our understanding of FRP and its role in hybrid controller design. They also discussed adding higher-order modeling capabilities to Ptolemy. Joern writes his summary: "At Yale, we met with John Peterson, Steven Morris, Paul Hudak, as well as some other members of Hudak's group (Antony Courtney, Walid Taha, Henrik Nilsson, Zhanyong Wan). After our presentation of Ptolemy (a talk and a demo), Antony Courtney showed us Frappe, which is a version of FRP that he uses to describe JavaBeans, and which he wants to automatically transform to Java (apparently that is work in progress). Afterwards, Wan and Nilsson showed us Frob, which is an application of FRP to robot control, complete with a small animation. All in all the response we got was positive. We had to overcome a little terminology mismatch (domain, model, and actor initially evoked wrong associations in Hudak's group, similar to FRP's behavior and event on our part), but eventually we think that we got our message across. It seems that the closest match for some interaction in the near future is Courtney's work on an FRP->Java translation. Hudak would be willing to send him over here for some time, and he certainly would be willing to come. Further areas of common interest are visualization (and in particular of higher-order functions). We did not have time to go very far into this, it seems Hudak is somewhat skeptical about visual languages in general, and their ability to express higher-order constructs in particular." * T. John Koo and Shankar Sastry taught a graduate course on "Hybrid Systems" in the Department of Electrical Engineering and Computer Sciences, UC Berkeley in 2001 spring semester. * T. Henzinger gave a talk on "Formal Verification of Embedded Systems" and a tutorial on HyTech at Scientific Systems in Woburn, Massachusetts (May 2001). * T. Henzinger gave a talk on "Model Checking of Infinite-state Systems" at Microsoft Research in Redmond, Washington (May 2001). * T. Henzinger gave a talk on "Giotto: A Time-triggered Language for Embedded Programming" at the Compaq Systems Research Center in Palo Alto, California (April 2001). * T. Henzinger, B. Horowitz, and C. Kirsch gave a full-afternoon tutorial on the Giotto approach at Wind River Systems in Alameda, California (April 2001). 3. Administrative Personnel --------- * Sonia Sachs has returned to LBL, but remains an (unpaid) visiting researcher. 4. Publications [1] R. Vidal, S. Schaffert, O. Shakernia, J. Lygeros, and S. Sastry, "Decidable and Semi-decidable Controller Synthesis for Classes of Discrete Time Hybrid Systems," to appear in IEEE Conf. on Decision and Control, Orlando, FL, December 2001. [2] T. J. Koo, G. J. Pappas, and S. Sastry, "Multi-Modal Control of Systems with Constraints," to appear in IEEE Conf. on Decision and Control, Orlando, FL, December 2001. [3] T. J. Koo, "Hierarchical System Architecture for Multi-Agent Multi-Modal Systems," to appear in IEEE Conf. on Decision and Control, Orlando, FL, December 2001. [4] T. J. Koo, J. Liebman, C. Ma, and S. Sastry, "Hierarchical Approach for Design of Multi-Vehicle Multi-Modal Embedded Software," EMSOFT 2001: First Workshop on Embedded Software, Lecture Notes in Computer Science, Springer-Verlag, 2001. [5] T. J. Koo, B. Horowitz, J. Liebman, C. Ma, R. Tal, and S. Sastry, "Hardware-in-the-loop Simulation of Multi-Vehicle Multi-Modal Embedded Systems," submitted to IFAC World Congress on Automatic Control, Barcelona, Spain, July, 2002. [6] Johan Eker, Chamberlain Fong, Jorn W. Janneck, Edward A. Lee and Jie Liu, "Design and simulation of heterogeneous control systems using Ptolemy II," accepted for presentation at the IFAC Conference on New Technologies for Computer Control (joint work with Mobies). [7] Edward A. Lee, "Embedded Systems" Technical Memorandum UCB/ERL M01/26, University of California, Berkeley, CA 94720, July 12, 2001 (joint work with Mobies). [8] Jie Liu, Stan Jefferson, and Edward A. Lee, "Motivating Hierarchical Run-Time Models in Measurement and Control Systems," 2001 American Control Conference, June 25-27, 2001, Arlington, VA, pp. 3457-3462. [9] Jie Liu, Xiaojun Liu, and Edward A. Lee, "Modeling Distributed Hybrid Systems in Ptolemy II," embedded tutorial in 2001 American Control Conference, June 25-27, 2001, Arlington, VA, pp. 4984-4985. [10] Xiaojun Liu, Yuhong Xiong, and Edward A. Lee, "The Ptolemy II Framework for Visual Languages," poster paper, (To appear in) Symposium on Visual Languages and Formal Methods, Stresa, Italy, Sept. 5-7, 2001 (joint work with Mobies). [11] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. From verification to control: dynamic programs for omega-regular objectives. Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001). [12] Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch. Embedded control systems development with Giotto. Proceedings of the ACM International Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES 2001). 4. Financial Data Provided separately on a quarterly basis by the university.