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: 1/1/02 - 3/31/01 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: in formal analysis, we solved the digital control problem for hybrid automata with _unknown_ sampling rate; in software design, we developed a methodology for designing embedded controllers for multi-vehicle, multi-modal systems; in control, we investigated the problem of formation flight. 1. Research Status Formal Modeling and Analysis ============================ From Models to Code: The Missing Link in Embedded Software ---------------------------------------------------------- Tom Henzinger and Christoph Kirsch developed a new methodology for producing validated embedded code. Much of hybrid systems design and validation happens at the level of mathematical models. While some tools offer automatic code generation from mathematical models, manual code optimization and integration is often necessary to achieve non-functional aspects such as concurrency, resource management, and timing. In the process, the tight correspondence between model and code is lost, raising the issue of implementation correctness and causing difficulties for code reuse. We submit that these problems can be alleviated by using an intermediate layer, which we call software model. A software model is closer to code than a mathematical model. While the entities of a mathematical model are, typically, matrices, equations, and perhaps state diagrams, the entities of a software model are data structures and procedures. For example, a software model may specify the representation for storing a matrix, the algorithm and precision for evaluating an equation, and the mechanism and time for communicating the result. However, a software model is more abstract than code. While code is executed by a particular OS and hardware platform, a software model is executed by a virtual machine. Common software models are high-level programming languages, but for embedded software, the model needs to include constructs for expressing concurrency and timing. A software model specifies the logical concurrency and interaction of processes, not the physical process distribution and communication protocol. Similarly, an embedded software model specifies the timing of process interactions with the environment, not the process schedules on a specific platform. For example, a software model may specify when a sensor is read, which sensor reading is used for computing an actuator value, and when the actuator is set, without specifying a CPU and priority for the computation. In short, a software model separates the platform-independent from the platform-dependent issues in embedded software development. The explicit use of a software model provides a great deal of flexibility in the optimization, integration, and reuse of embedded components. By orthogonalizing concerns, it also facilitates improved code generation and formal verification. One possible software model is Giotto, which is designed for high-performance control applications, but different design decisions can lead lead to software models with different characteristics. A comparison of control problems for timed and hybrid systems ------------------------------------------------------------- In the literature, we find several formulations of the control problem for timed and hybrid systems. Tom Henzinger, Frank Cassez, and J-F Raskin showed that formulations where a controller can cause an action at any point in dense (rational or real) time are problematic, by presenting an example where the controller must act faster and faster, yet causes no Zeno effects (say, the control actions are at times 0, 1/2, 1, 1 1/4, 2, 2 1/8, 3, 3 1/16, ... Such a controller is, of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well-understood if the time unit, or "sampling rate" of the controller, is fixed a priori, a novel, stronger formulation can be defined: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We have proved that this problem is undecidable even in the special case of timed automata. Embedded Software Design ======================== Caltech Platform ---------------- We continue to work with Caltech on their rolling platform driven by two ducted fans. In particular, Steve Neuendorfer visted Caltech and constructed a detailed model in Ptolemy II of the platform, and designed, jointly with Caltech personnel, a controller that drives the platform from one position to another. In anticipation of experimenting in-house with a version of the platform, Paul Yang and David Lee have set up a video-based localization prototype that will enable detection of the location of the platform within a room. Their prototype uses colors rather than shapes to minimize computational load. It is implemented in Java using Sun's Java Media Framework. Platform-Based Embedded Software Design for Multi-Vehicle Multi-Modal Systems ----------------------------------------------------------------------------- T. John Koo, Judith Liebman, Cedric Ma, Benjamin Horowitz, Alberto Sangiovanni-Vincentelli, Shankar Sastry presented a methodology for the design of embedded controllers for multi-vehicle multi-modal systems. The methodology is predicated upon the principles of platform-based design, which uses layers of abstraction to isolate applications from low-level system details and yet provides enough information about the important parameters of the lower layers of abstraction, to modularize the system design and to provide predictable system performance. An essential layer of abstraction in our methodology is the software platform provided by the programming language Giotto, which allows a clean implementation of a time-based controller application. The methodology includes a hardware-in-the-loop simulation framework, in which system components can be replaced by actual implementation for high-fidelity simulation. To demonstrate the effectiveness of our design methodology, a helicopter-based unmanned aerial vehicle system is presented. They present simulation results which validate the quality of our embedded control system implementation, and we extend the framework to apply to multiple UAVs in a flight formation. Controller Design and Analysis ============================== A Roadmap for Formation Flight of Autonomous Vehicles ----------------------------------------------------- T. John Koo, Jin Kim, Shannon Zelinski, and Shankar Sastry studied the enabling components for enabling formation flight of autonomous vehicles. There are three major tasks which are necessary in order to make formation possible and they are formation generation, formation initialization, and formation control. Formation generation task generates a set of feasible formations where each formation satisfies multiple constraints including vehicle dynamics, communication, and sensing capabilities. Given an initial and a final formation for a group of autonomous vehicles, formation initialization problem is to generate collision-free and feasible trajectories and to derive control laws for the vehicles to track the given trajectories simultaneously in finite time. Formation control of multiple autonomous vehicles focus on the control of individual agents to keep them in a formation, while satisfying their dynamic equations and inter-agent formation constraints, for an underlying communication protocol being deployed. Hybrid Control Design for Formation Flight ------------------------------------------ Shannon Zelinski and T. John Koo formulated the problem of formation generation as a hybrid system synthesis problem. By considering dynamic and formation constraints, a Formation Mode Graph is constructed. For each formation, information about the formation is computed offline and is stored in each node of the graph. Feasible transition between formations are specified by edges. Given an initial formation, any feasible formations can be efficiently searched on the graph. Nonlinear Model Predictive Planning and Control ----------------------------------------------- H. Jin Kim presented nonlinear model predictive planning & control framework which combines trajectory planning and control into a single problem, using ideas from potential-field based navigation for real-time path planning and nonlinear model predictive control for optimal control of nonlinear multi-input, multi-output systems with input/state constraints. She incorporates a tracking performance, potential function, state constraints into the cost function to minimize, and use gradient-descent for on-line optimization. A scenario with three UAVs which are given straight line trajectories that will lead to collision is considered. By using the framework, the safe trajectory of the vehicles are dynamically replanned and tracked by the vehicles under input saturation and state constraints. 2. Interactions and Technology Transfer Presentations ------------- * Edward A. Lee, "Preventing the use of Commercial Aircraft as Weapons," invited talk, Institute of Transportation Studies, UC Berkeley, February 8, 2002. * Steve Neuendorffer, "Heterogenous Actor-oriented Modeling in Ptolemy II," UC Irvine, Feb. 21, 2002. * Wolfgang Pree and Christoph Kirsch, "Integration of Giotto and Simulink Embedded Software Seminar," Embedded Software Seminar, UC Berkeley, February 25, 2002. * T. John Koo and S. Sastry "Bisimulation Based Hierarchical System Architecture for Single-Agent Multi-Modal Systems" 5th International Worshop, Hybrid Systems: Computation and Control, Stanford, CA, USA March 2002. * Tom Henzinger, "From Models to Code: The Missing Link in Embedded Software", Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC 02), invited talk, Stanford, California (March 2002). * Thilo Demmeler, "Enabling Rapid Design Exporation through Virtual Integration and Simulation of Fault Tolerant Automotive Application" Embedded Software Seminar organized by T. John Koo, University of California at Berkeley, January 23, 2002. * Wolfgang Pree and Christoph Kirsh "Integration of Giotto and Simulink" Embedded Software Seminar organized by T. John Koo, University of California at Berkeley, February 25, 2002. * Gerardo Schneider, VERIMAG, France "Algorithmic analysis of polygonal piecewise constant differential inclusions", Embedded Software Seminar organized by T. John Koo, University of California at Berkeley, March 22, 2002. Interactions ------------ * Wolfgang Pree, Professor at the University of Salzburg, Austria, and Christoph Kirsch of UC Berkeley worked together to integrate Giotto and Simulink. Simulink is used as a front-end for building Giotto designs, and a tool then translates these into another Simulink model that executes with Giotto semantics. Technology Transfer ------------------- * We have organized a new course, taught during the current semester, Spring 2002. EE290N: Advanced topics in systems theory: Concurrent models of computation Instructor: Prof. Edward A. Lee This experimental research course will study models of computation used for the specification and modeling of concurrent systems, particularly those with relevance to embedded and real-time systems design. Current research approaches will be considered, including the tagged signal model, behavioral type systems, interface theories, and (possibly) category theoretic approaches. The emphasis will be on developing an understanding of models of computation in practical use and of the mathematical tools that researchers can use to study them. The course will begin with a review of the theory of partially ordered sets, particularly as applied to prefix orders and Scott orders. It will develop a framework for models of computation for concurrent systems that uses partially ordered tags associated with events. Discrete-event models, synchronous/reactive languages, and dataflow models will be studied in this context. Basic issues of computability, boundedness, determinacy, liveness, and the modeling of time will be studied. Classes of functions over partial orders, including continuous, monotonic, stable, and sequential functions will be considered, as will semantics based on fixed-point theorems. A hieararchy of increasingly specialized asynchronous models of computation, including process networks, Kahn process networks, dataflow process networks, the Boolean dataflow model, and synchronous dataflow will be covered. Timed models, including discrete-event systems (as embodied for example in the VHDL and Verilog languages) and the synchronous/reactive languages Signal, Lustre, Esterel, and Statecharts will be studied. * We have organized a new course, taught during the current semester, Spring 2002. EE291E: Hybrid Systems, Spring 2001. Instructors: Dr. T. John Koo and Prof. S. Shankar Sastry Course description: The multi-disciplinary research field of hybrid systems has emerged over the last decade and lies at the boundaries of computer science, control engineering and applied mathematics. In general, a hybrid system can be defined as a system built from atomic discrete components and continuous components by parallel and/or serial composition, arbitrarily nested. The behaviors and interactions of components are governed by models of computation. The hybrid phenomena captured by such mathematical models are manifested in a great diversity of complex engineering applications such as real-time systems, embedded software, robotics, mechatronics, aeronautics, and process control. The high-profile and safety-critical nature of such applications has fostered a large and growing body of work on formal methods for hybrid systems: mathematical logic, computational models and methods and automated reasoning tools supporting the formal specification and verification of performance requirements for hybrid systems, and the design and synthesis of control programs for hybrid systems that are provably correct with respect to formal specifications. This course investigates modeling, analysis and synthesis of various classes of hybrid systems. An introduction to computational and simulation tools for hybrid systems will be given. The course consists of lectures, a handful of homeworks, and a final project. * We have organized a new course, taught during the current semester, Spring 2002. EE290o: Embedded Software Engineering Instructor: Christoph Kirsch Brief Overview: This 3 unit course will provide an introduction to embedded software engineering: the first part covers real-time operating systems, real-time communication protocols, and scheduling theory; the second part focuses on real-time programming and code generation. The course is a revised version of a course that has been held in Spring 2001 for the first time. The course begins with an introduction to real-time operating system concepts and real-time communication protocols like the time-triggered protocol (TTP) and the event-triggered CAN protocol. Scheduling techniques like rate-monotonic and earliest deadline first scheduling will be illustrated. The second half of the course emphasizes real-time programming and code generation for embedded systems. The high-level embedded programming languages Esterel, Lustre, and Giotto, will be presented. Esterel and Lustre are so-called synchronous reactive languages. Giotto is a time-triggered programming language for embedded control systems that has recently been developed at UC Berkeley. Code generation for Giotto will be discussed based on a virtual machine architecture called the embedded machine that has also been developed at UC Berkeley. Example programs in Esterel, Lustre, and Giotto will be implemented on Lego Mindstorm robots. Each week, a one and a half hour lecture will be presented and a one and a half hour discussion will be held. Personnel --------- Johan Eker, postdoc, has finished his stay at Berkeley and returned to Sweden. 4. Publications [1] Jie Liu and Edward A. Lee, "Timed Multitasking for Real-Time Embedded Software," invited paper to IEEE Control System Magazine, draft version, January 31, 2002. http://ptolemy.eecs.berkeley.edu/publications/papers/02/timedmultitasking/ [2] Jie Liu, Johan Eker, Xiaojun Liu, John Reekie, and Edward A. Lee, "Actor-Oriented Control System Design," invited paper to IEEE Transactions on Control System Technology, draft version, March 15, 2002. http://ptolemy.eecs.berkeley.edu/publications/papers/02/actorOriented/ [3] Stephen A. Edwards and Edward A. Lee,"The Semantics and Execution of a Synchronous Block-Diagram Language," accepted by Science of Computer Programming, to appear, 2002. http://ptolemy.eecs.berkeley.edu/papers/02/blockdiagram2/ [4] Johan Eker, Chamberlain Fong, Jorn W. Janneck, and Jie Liu, "Design and Simulation of Heterogeneous Control Systems using Ptolemy II," IFAC Conference on New Technologies for Computer Control (NTCC'01), Hong Kong, China, Nov. 2001. [5] Jie Liu, Johan Eker, Jorn W. Janneck, Edward A. Lee, "Realistic Simulations of Embedded Control Systems", accepted to International Federation of Automatic Control 15th IFAC World Congress Barcelona, Spain July 21-26, 2002. [6] T. John Koo, Judith Liebman, Cedric Ma, Benjamin Horowitz, Alberto Sangiovanni-Vincentelli, Shankar Sastry, "Platform-Based Embedded Software Design for Multi-Vehicle Multi-Modal Systems", submitted to Embedded Software Conference (EMSOFT'02), Grenoble, France, 2002. [7] Benjamin Horowitz, Judith Liebman, Cedric Ma, T. John Koo, Alberto Sangiovanni-Vincentelli, Shankar Sastry, "Platform-Based Embedded Software Design and System Integration for Autonomous Vehicles," submitted to IEEE Proceedings, March 2002. [8] Franck Cassez, Thomas A.~Henzinger, J.-F.~Raskin, "A comparison of control problems for timed and hybrid systems," Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC 02), Lecture Notes in Computer Science, Springer-Verlag, 2002. 5. Financial Data Provided separately on a quarterly basis by the university.