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/00 - 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. The major contribution in this reporting period has been in the synchronous modeling formalism Massachio and the associated language Giotto. This formalism and language have time-driven semantics, inspired by TTA, but with an eye towards verifiability and efficient, retargettable implementations. We have defined a textual syntax for Giotto and and associated compiler, and have built a Ptolemy II domain with Giotto semantics. We are currently exploring the programmer's model using and comparing these two implementations to learn about certain subtleties in the formalism. We also obtained several novel results in multi-modal and multi-agent control based on hybrid systems models. 1. Research Status Formal Modeling and Analysis ============================ We continued to work out the hierarchical specification formalism Masaccio for hybrid systems, and its refinement into time-triggered Giotto programs. Two papers have been submitted on this topic to the hybrid systems 2001 workshop; they will be described in detail when the final versions become available. In addition, we obtained results in three areas described below. First, we developed a control theory for systems with synchronous communication, such as rendezvous-based message passing [10]. Second, we used control-based game-theoretic techniques to lead to the quicker detection of errors in model checking [11]. Finally, we unified decidability results about discrete abstractions of hybrid systems by integrating results about systems with simple discrete dynamics and results about systems with simple continuous dynamics [12]. The Control of Synchronous Systems [10] ---------------------------------- In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their effects on the control problem. A static type enforces fixed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process and control objective, there may be a controller of a static type, or only a controller of a syntactically compatible dynamic type, or only a controller of a semantically compatible dynamic type. We show this to be a strict hierarchy of possibilities, and we present algorithms and determine the complexity of the corresponding control problems. Furthermore, we consider versions of the control problem in which the type of the controller (static or dynamic) is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more Detecting Errors before Reaching Them [11] ------------------------------------- Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs; for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated. The key observation is that "unpreventability", is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of "unpreventability," including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol. Discrete Abstractions for Hybrid Systems [12] ---------------------------------------- A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analyzed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas. Embedded Software Design ======================== The objective of this part of the project is to adapt sophisticated software techniques to the problem domain of real-time control systems. The problem domain mandates a priority on real-time guarantees and verifiable designs. Our approach is based on formalizing the models of computation that govern the interaction between components (both hardware and software components), and building software that realizes these models of computation. Control systems integrate a variety of hardware, including networked sensors and actuators, with variety of service demands, ranging from hard-real-time signal processing to interaction with human operators. Hence, our approach emphasizes the composition of heterogeneous models of computation. Giotto - A time-triggered language for embedded programming ----------------------------------------------------------- Giotto is a programming language to describe the behavior of distributed real-time embedded systems. Giotto has a formally defined time-triggered semantics which supports embedded programming at a high level of abstraction. In fact, a Giotto program provides an architecture-independent and thus logical view of an embedded system. Giotto program consists of a set of modes where each mode contains a set of tasks. A distributed embedded system described by a Giotto program can only be in a single mode at the same time. The decision to perform a mode switch is based on sampling changes in the environment. Future objectives are formal verification of real-time properties of Giotto programs using a refinement relation to the modeling language Masaccio, as well as annoted versions of Giotto allowing for architecture-dependent refinements of Giotto. Hardware Setup -------------- Ben Horowitz reports a first success with the Compulab boards, wireless Ethernet, and VxWorks. The Compulab boards are 486 single board computers. They are roughly the size of credit cards. He has installed VxWorks on a Compulab board. Each board communicates with a Windows NT machine via wireless Ethernet. Upon booting, the board uses ftp to download an executable VxWorks image. He is able to monitor and control the board from the NT machine, can start and stop tasks, download and run object files, and can view detailed timing data. Giotto Implementations ---------------------- Ben and Christoph Meyer have developed a timed embedded operating system called Grt that they now run on these boards. Grt implements the semantics of Giotto, the time-triggered programming language that the Fresco group has been developing. In a parallel effort, Christoph Meyer and Edward Lee created a Giotto domain in Ptolemy II. This offers a visual syntax for specifying Giotto programs, and a heterogeneous modeling environment, where Giotto programs can include components that are designed using some other formalism, such as dataflow. The Ptolemy II domain offers a hierarchical mode switch structure, and a method to specify architecture dependent information. We are investigating the depth of the match to Giotto semantics. Xioajun Liu built a simple hierarchical model with Giotto and FSM (finite-state machine) domains that illustrates this hierarchical mode switching. Lego Application ---------------- Christoph Meyer defined a simple application using Lego robots that illustrates well some of the key features of Giotto. In his realization, each robot has two motors and a touch sensor. The Giotto program does the following. There is a one leader among the robots. That leader chooses randomly between moving forward or backward and stopping. If a touch sensor on any robot is pushed, then that robot stops all the robots, performs an evasive maneuver, and then becomes the leader. We have implemented this example in three distinct ways: using "not quite C" on the Lego robots to implement the Giotto program, using C programs running on the Compulab boards (done by Ben Horowitz), and using a Ptolemy II model in the Giotto domain (done by Xioajun Liu). Run-Time Models for Measurement and Control Systems --------------------------------------------------- During his summer internship at Agilent Labs, Jie Liu made considerable progress on run-time models for measurement and control systems and their support in Ptolemy II. The models are assumed to execute on computational nodes in distributed measurement and control systems. Jie extended some existing domains in Ptolemy II, converting them from design-time modeling framelets (small frameworks), to run-time execution environments. He has started a new process-based domain that uses priority-based dynamic scheduling (see next item). He has also adapted the discrete-event modeling of Ptolemy II to support a real-time-based model (time synchronized discrete event). This leverages the global time synchronization provided in Agilent's smart sensors hardware. Jie has given two demos, a measurement system and a control system, that use Agilent NCAPs (network capable application processors), the time-sync protocol, and Ptolemy II. Real-Time Processes ------------------- Jie Liu has developed a preliminary prototype of a new process oriented domain for Ptolemy II that he called "real-time processes" (RTP). This domain is designed for control-oriented embedded systems. These systems usually have instrumentation interface for physical plants. The sensor and actuator processes usually runs independently from the control processes. The interaction between these processes are usually through I/O mapped address or interrupts. The RTP domain is a process-oriented domain, where each actor in the domain is a separate thread of execution. The receivers in this domain are capacity-one mailboxes. Tokens in the receivers are consumed by the actor by calling the get() method on the receiver. The get() method is blocking, in the sense that if there is no token in a receiver, the actor's execution thread will be blocked until a new token is delivered to the receiver. If a new token is put into the receiver before the old token is consumed, the old tokens is overwritten by the new one. That is, the consumer threads always deal with the newest data. The domain can potentially make use of the real-time properties provided by RTOS. For example, priorities or rate-monotonic properties can be assigned to each actor (thread). The execution of the actors then depends on the real-time scheduling of the RTOS. The underlying RTOS could be a real one or a simulated one. The ease of transferring the model from design-time to run-time could be a strength of the domain. Controller Design and Analysis ============================== We have been investigating many issues relating to controller synthesis and verification of real time multi-agent multi-modal control systems on embedded platforms. Hybrid system theory provides powerful tools to model, design, and analyze complex control systems such as the multi-agent multi-modal system. For these reasons, we have been extensively studying properties of hybrid systems and controller synthesis techniques for this framework. In particular, we have been studying the utility of hybrid systems for modeling systems, synthesizing mode generation controllers, and synthesizing optimal controllers. Techniques for high-level strategic planning controllers have also been investigated. In parallel to these studies, control software has been developed on an experimental test bed. The objective is to use these models and techniques to design and analysis multi-agent multi-modal control systems requiring high levels of mission reliability in a dynamic and rapidly evolving environment. Hybrid System Models -------------------- Hybrid systems have provided a extensive framework for furthering our understanding of multi-agent multi-modal controllers. We have been working towards continuing to enrich the hybrid framework in many ways. Jianghai Hu has studied controller synthesis as an application of geodesics in Riemannian Manifolds with boundaries. Using this framework, he has studied generating controllers which avoid conflict between agents in a multi-agent system. Jun Zhang, Karl Johansson, John Lygeros, and Shankar Sastry have extended several important results of classical dynamical systems to hybrid dynamical systems. Most notably, the issue of Zeno executions have been investigated. Slobodan Simic, Karl Johansson, John Lygeros, and Shankar Sastry have continued to work on a new geometric framework for hybrid systems. Ekaterina Lemch has studied the extension of controllability to hybrid systems in this geometric framework. Multi-Modal Controller Synthesis -------------------------------- John Koo, Shankar Sastry and George Pappas of University of Pennsylvania have been working on mode switching synthesis for specifications which are based on mission completion properties. In particular, they are interested in reachability specifications at this point. The objective is to develop a general framework for the study of control mode switching and algorithms for the derivation of sequences of control modes which will satisfy reachability tasks. They hope to implement the algorithms based on existing efficient = methods for reachability computation and apply the algorithms to certain classes of dynamical systems. Optimal Hybrid Controller Synthesis ----------------------------------- Using the hybrid framework, we can develop controllers satisfying several important properties such as minimum energy, least restrictive, and safeness. Omid Shakernia, George Pappas, and Shankar Sastry have investigated least restrictive controller synthesis for hybrid systems with reachability constraints. In particular, they have studied conditions under which this problem is decidable. Magnus Egerstedt, Petter Ogren, Omid Shakernia, John Lygeros have studied synthesis of controllers that drive hybrid systems from one state to another state. They have focused on the number of mode changes necessary for such a controller. Rene Vidal, Shawn Schaffert, John Lygeros, and Shankar Sastry have investigated an extension of least restrictive controller and maximal controlled invariant set synthesis to hybrid systems with safety constraints. In addition, they have studied nonlinear extensions and decidability issues. Jianghai Hu and Ekaterina Lemch have been studying methods to generate tight smooth approximations of hybrid systems. Using the approximate system, tradition techniques of optimal control can be investigated. UAV Control Software Development -------------------------------- Developing a low level controller that is stable and responsive is critical for facilitating more complex controller designs. David Shim has been constructing both a pid and a mu-synthesis controller for several different embedded helicopter platforms. He has achieved stability and wave point navigation. In addition, David Shim has been preparing a helicopter for the open control platform (OCP). On this embedded platform, the OCP will be used to provide a rigorous, dependable environment on which the previously mentioned hybrid multi-modal controller synthesis techniques can be implemented. Multi-Agent Strategic Controller -------------------------------- Building more advanced control strategies on top of the low level controller will provide a system with better performance and the ability to adapt to a rapidly changing environment. In particular, in a multi-agent scenario it is important to design controllers that can utilize pursuit and evasion strategies. Hyoun Jin Kim has been studying the different kinds of game playing policies that are most effective for this framework. 2. Interactions and Technology Transfer * August 14, 2000: Informal meeting with Helen Gill. We gave an overview of progress on the Ptolemy II effort, including demonstrating the graphical user interface, and an overview of work in time-driven models for hard-real-time systems. * June-August, 2000, Jie Liu served as an intern at Agilent Labs and worked on smart, networked sensors. * "Frameworks for Discrete-Event Modeling and Design," Edward A. Lee, invited talk, Control Systems Seminar, Univ. of Michigan, Ann Arbor, September 29, 2000. * "The Gigascale Silicon Research Center," Report on the GSRC Semantics Project, Jorn Janneck, SLDL meeting, San Jose, CA, September 21, 2000. * "Concurrent Models of Computation in System-Level Design," invited plenary talk, Edward A. Lee, Forum on Design Languages (FDL), Tubingen, Germany, September 7, 2000. * "The Gigascale Silicon Research Center," Report on the GSRC Semantics Project, Edward A. Lee, Forum on Design Languages (FDL), Tubingen, Germany, September 6, 2000. * "What Comes After C++ in System-Level Specification," Panel Discussion, Edward A. Lee, Forum on Design Languages (FDL), Tubingen, Germany, September 6, 2000. * "Discrete-Event Modeling and Design of Embedded Software," invited plenary talk, Edward A. Lee Workshop on Discrete Event Systems, WODES 2000, Ghent, Belgium, 21-23 August, 2000. * "Ptolemy II - Heterogeneous Modeling and Design in Java," Edward A. Lee, July 6, 2000, Agilent Labs, Palo Alto, CA. * "Run-Time Models for Measurement and Control Systems and Their Support in Ptolemy II," Jie Liu, August 23, 2000, Agilent Labs, Palo Alto, CA. * "Reactive System Synthesis of UAV Flight Management System," Jie Liu,at the Unmanned Air Vehicle: Coordinations, Sensing, and Control Workshop, Sept. 24, 2000, Anchorage Hilton, Anchorage, Alaska. * T. John Koo is currently visiting University of Pennsylvania as a Visiting Research Fellow and will return to Berkeley in January 2001 to continue research on Multi-Modal Control. * Slobodan Simic is teaching a graduate course on Advanced Topics in Nonlinear Control and Hybrid System Theory at the University of California, Berkeley. * "Fresco: Formal Real-time Software Components", invited talk, First Workshop on Models for Time-critical Systems (MTCS 00), State College, Pennsylvania (August 2000). * "Masaccio: A Formal Model for Embedded Components", invited talk, First IFIP International Conference on Theoretical Computer Science (TCS 00), Sendai, Japan (August 2000). 3. Publications [1] Jie Liu and Edward A. Lee, "Component-based Hierarchical Modeling of Systems with Continuous and Discrete Dynamics," Proc. of the 2000 IEEE International Conference on Control Applications and IEEE Symposium on Computer-Aided Control System Design (CCA/CACSD'00), Anchorage, AK, September 25-27, 2000. pp. 95-100. [2] Jie Liu, Stan Jefferson, and Edward A. Lee, "Run-time models for measurement and control systems, and their support in Ptolemy II," submitted to 2001 American Control Conference, invited session on Software Enabled Control, June 2001, Arlington, VA. [3] M. Egerstedt, P. Ogren, O. Shakernia, J. Lygeros, "Toward Optimal Control of Switched Linear Systems," M. Egerstedt, Proceedings of 39th IEEE Conf. on Decision and Control, Sydney, AU, December 2000 [4] T. John Koo, "Hybrid System Design and Embedded Controller Synthesis for Multi-Modal Control," PhD Thesis, EECS Dept., University of California, Berkeley, August, 2000. [5] T. John Koo, George J. Pappas, and S. Shankar Sastry, "Mode Switching Synthesis for Reachability Specifications," submitted to HSCC2001. [6] Omid Shakernia, George J. Pappas, Shankar Sastry, "Semidecidable Controller Synthesis for Classes of Linear Hybrid Systems," Proceedings of 39th IEEE Conf. on Decision and Control, Sydney, AU, December 2000. [7] Omid Shakernia, George J. Pappas, Shankar Sastry, "Semi-decidable Synthesis for Triangular Hybrid Systems, " Submitted to Hybrid Systems: Computation and Control, Rome, Italy, March 28-31, 2001. [8] Rene Vidal, Shawn Schaffert, John Lygeros, and Shankar Sastry, "Decidable and Semi-decidable Controller Synthesis for Discrete Time Hybrid Systems," submitted to HSCC2001. [9] Jun Zhang, Karl Henrik Johansson, John Lygeros, and Shankar Sastry, "Zeno Hybrid Systems," to appear in Special Issue on Hybrid Systems of the International Journal of Robust and Nonlinear Control. [10] Luca de Alfaro, Thomas A. Henzinger, F.Y.C. Mang, "The control of synchronous systems", Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 00), Lecture Notes in Computer Science 1877, Springer-Verlag, 2000, pp. 458-473. [11] Luca de Alfaro, Thomas A. Henzinger, F.Y.C. Mang, "Detecting errors before reaching them", Proceedings of the 12th International Conference on Computer-aided Verification (CAV 00), Lecture Notes in Computer Science 1855, Springer-Verlag, 2000, pp. 186-201. [12] Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, George J. Pappas, "Discrete abstractions of hybrid systems", Proceedings of the IEEE 88, 2000, pp. 971-984. 4. Financial Data Provided separately on a quarterly basis by the university.