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/03 - 6/30/03 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: we developed and evaluated the concept of schedule carrying code, where embedded software is annotated with scheduling instructions for improved scheduling flexibility and performance; we formalized the notion of causality in hybrid and mixed-signal systems and analyzed the implications in their denotational semantics; we realized mobile models, where models are transported in XML using CORBA, to implemented distributed control, and demonstrated its use on the Caltech ducted fan vehicle; and we identified a need for interface definitions that convey causality information and began work on developing a suitable interface theory. 1. Research Status Formal Modeling and Analysis ============================ The Element of Surprise in Timed Games -------------------------------------- The control of real-time and hybrid systems is naturally formulated and solved as timed games (controller versus plant). We developed a symmetric formulation of such timed games and provided the corresponding control algorithms. We considered concurrent two-person games played in real time, in which the players decide both which action to play, and when to play it. Such timed games differ from untimed games in two essential ways. First, players can take each other by surprise, because actions are played with delays that cannot be anticipated by the opponent. Second, a player should not be able to win the game by preventing time from diverging. We presented a model of timed games that preserves the element of surprise and accounts for time divergence in a way that treats both players symmetrically and applies to all omega-regular winning conditions. We proved that the ability to take each other by surprise adds extra power to the players. For the case that the games are specified in the style of timed automata, we provided symbolic algorithms for their solution with respect to all omega-regular winning conditions. We also showed that for these timed games, memory strategies are more powerful than memoryless strategies already in the case of reachability objectives. Schedule Carrying Code ---------------------- To guarantee the correct execution of a hard real-time program on a given platform, the scheduler must ensure that all deadlines are met. We introduced the paradigm of schedule-carrying code (SCC), where the compiler proves the existence of a feasible schedule by generating such a schedule, which is then attached to the generated code in the form of executable instructions that remove the need for a system scheduler. In this way, the schedule is produced once, and revalidated and executed with each use. We evaluated SCC both in theory and practice. In theory, we gave two scenarios, of nonpreemptive and distributed scheduling for Giotto programs, where the generation of a feasible schedule is hard, while the validation of scheduling instructions that are attached to the code is easy. In practice, we implemented SCC and show that explicit scheduling instructions can reduce the scheduling overhead up to 35 percent, and can provide an efficient, flexible, and verifiable means for compiling Giotto on complex architectures, such as the TTA. Causality in Mixed-Signal and Hybrid Systems -------------------------------------------- Together with Jie Liu of PARC, we have completed a study of the semantics of causality in mixed-signal and hybrid models [6]. This study extends the application of the Cantor metric as a mathematical tool for defining causality from purely discrete models to mixed-signal and hybrid models. Using the Cantor metric, which represents timed signals, continuous or discrete, in a metric space, we define causality as contractive properties of processes operating on these signals. Thus, the Banach fixed point theorem can be applied to establish conditions for the existence, uniqueness, and liveness of the behaviors for mixed-signal and hybrid systems. The results also provide theoretical foundations for the simulation technologies for such systems, including the time-marching strategy, evaluation of feedback loops, and the necessity of supporting rollback. Embedded Software Design ======================== Mobile Models and the Caltech Vehicle ------------------------------------- Steve Neuendorffer has demonstrated the use of Ptolemy II for designing controllers for the Caltech ducted fan vehicle. Four configurations have been shown: (1) the controller and vehicle are both simulated; (2) the controller is code-generated and the generated code interacts with a simulation of the vehicle (hardware in the loop simulation); (3) the controller is simulated and interacts with the physical vehicle (simulation-based rapid prototyping); and (4) the controller is code-generated and the generated code interacts with the physical vehicle (deployment). To facilitate experimentation with control algorithms, Yang Zhao developed a MobileModel Ptolemy II actor, which is a higher-order actor that accepts a model definition at one of its input ports, and then executes that model to process data provided at the other input ports. The prototype application of this concept uses a Ptolemy II model on the vehicle with the MobileModel actor implementing the control laws, and a separate supervisory model on another laptop providing the control laws over a CORBA channel (using a wireless network). A key issue for such mobile models is security. Currently, the prototype accepts models provided in cleartext XML and makes no distinction between models that use actors that convey authority (e.g. actors that read or write local files) and models with no such actors. An essential next step is to develop a security policy for mobile models that enables secure (encrypted) transport of digitally signed executable models and regulated granting of authority to such models. Hierarchical Hybrid Systems Models ---------------------------------- With support from the Mobies program and from NSF, the Ptolemy group at Berkeley developed a "hybrid systems visual modeler" called HyVisual. HyVisual is based on Ptolemy II. As part of the SEC effort, HyVisual has been used to construct various hybrid systems models, and a key semantic issue has been identified (by John Koo). HyVisual starts with Simulink-like block-diagrams that represent ordinary differential equations. Unlike Simulink, it does not attempt to solve algebraic equations, but rather requires that any directed loop in the model include at least one integrator. This is sufficient to ensure that the execution trace is uniquely defined, at least denotationally (that is, that the denotational semantics is determinate, see [6]). HyVisual augments ODEs with modal models, where a finite-state machine governs discrete switching between modes, and each mode represents a subsystem (called the "refinement" of the mode). The refinement can be a continuous-time model, a discrete model, or a memoryless computation; the information hiding software architecture of Ptolemy II ensures consistent behavior across such heterogeneous models. However, this same information hiding prevents the solver at one level of the hierarchy from knowing the causality properties of another level of the hierarchy. We have begun working on an abstract representation of causality properties that can be exposed as an interface definition across levels of the hierarchy, and that can be composed so that in a modal model with multiple refinements, the interfaces of the refinements can be merged to define an interface of the modal model. This method will apply not only to the continuous-time ODE-based modeling of HyVisual, but also to discrete-event modeling, synchronous/reactive modeling, and constraint-based models of computation. More information about HyVisual can be found at: http://ptolemy.eecs.berkeley.edu/hyvisual/ Localization Technology ----------------------- David Lee and Paul Yang completed their Ptolemy II implementation of a video-based localization technique for the Caltech ducted fan vehicle. This localization program uses a webcam and JMF (the Java Media Framework). It uses color segmentation to track the vehicle. Two separate color dots are placed on the cart, with one color used for position and a different color for rotation. During this reporting period, David and Paul implemented: 1) Automatic Color Calibration using a histogram. 2) Distance calculations based on pixel information. Controller Design and Analysis ============================== Formation Reconfiguration For Autonomous Vehicles ------------------------------------------------- Coordination of multiple unmanned aerial vehicles (UAVs) poses significant theoretical and technical challenges. Recent advances in sensing, communication and computation enable the conduct of cooperative multiple-UAV mission deemed impossible in the recent past. T. John Koo, Shannon Zelinski and Shankar Sastry worked on solving the Formation Reconfiguration Planning (FRP) problem which is focused on determining a nominal state and input trajectory for each vehicle such that the group can start from the given initial configuration and reach its given final configuration at the specified time while satisfying a set of given inter- and intra- vehicle constraints. Each solution of a FRP problem represents a distinct reconfiguration mode. When coupled with formation keeping modes, they can form a hybrid automaton of formation maneuvers in which a transition from one formation maneuver to another formation maneuver is governed by a finite automaton. We show a simulation results of a group of 9 UAVs performing a sequence of formation reconfigurations. Collision Avoidance based on Nonlinear Model Predictive Control --------------------------------------------------------------- H. Jin Kim presented nonlinear model predictive planning and 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. Platform-Based Embedded Software Design --------------------------------------- B. Horowitz used the concepts of platform-based design to develop a methodology for the design of automatic control systems that built in modularity and correct-by-construction procedures. The use of platform-based design allows us to build a bridge between the time-based controller application and the non-time-based sensors and actuators. A time-based controller eliminates the timing irregularities present in first generation system. Further, the Giotto compiler ensures that the controller application meets its timing requirements. Our platform-based design achieves a high degree of modularity. 2. Interactions and Technology Transfer Presentations ------------- Christoph Kirsch. Principles of real-time programming. EmSys Summer School, Salzburg, Austria, June 2003. Christoph Kirsch. Real-time programming based on schedule-carrying code. University of Pennsylvania, Philadelphia, PA, April 2003. Christoph Kirsch. Real-time programming based on schedule-carrying code. University of California, Irvine, CA, April 2003. Christoph Kirsch. Real-time programming based on schedule-carrying code. EPFL, Lausanne, Switzerland, May 2003. Thomas A. Henzinger. Discounting the future in systems theory. At the 30th International Colloquium on Automata, Languages, and Programming (ICALP), Eindhoven, The Netherlands, June 2003. Thomas A. Henzinger. Counterexample-guided control. At the 30th International Colloquium on Automata, Languages, and Programming (ICALP), Eindhoven, The Netherlands, June 2003. Krishnendu Chatterjee. Stack size analysis for interrupt-driven programs. At the 10th International Static Analysis Symposium (SAS), Los Angeles, California, June 2003. T. John Koo. Hybrid System Design for Autonomous Vehicles. Honeywell Aerospace Electronics Systems, Technology Centers of Excellence, Minneapolis, Minnesota, March 6, 2003. T. John Koo. Hybrid System Design for Autonomous Vehicles. Department of Aerospace Engineering Sciences, University of Colorado at Boulder, Boulder, CO, March 17, 2003. T. John Koo. Hybrid System Design for Autonomous Vehicles. Department of EECS, Vanderbilt University, Nashville, TN, March 27, 2003. T. John Koo. Hybrid System Design for Autonomous Vehicles. Control System Group Seminar, MIT, Cambridge, MA, May 2, 2003. T. John Koo. Formation Reconfiguration for Autonomous Vehicles. AHS 59th Annual Forum and Technology Display "Vertical Flight Transformations," Phoeniz, AZ, May 6-8, 2003. Edward A. Lee. Mobies Ethereal Sting OEP The Ptolemy II Experiment. Ethereal Sting Working Group Meeting, June 10, 2003, Arlington, VA Technology Transfer ------------------- We held the Fifth Biennial Ptolemy Miniconference, where technology developed with SEC funding was showcased together with other work. The Miniconference was held on Friday, May 9, 2003, at the Claremont Hotel, Berkeley and was attended by 90 people from 43 organizations worldwide. The presentations are available at: http://ptolemy.eecs.berkeley.edu/conferences/03/ The program included the following presentations and posters: - Project Status and Overview, Edward A. Lee, UC Berkeley - SimWORKS, A hybrid Java/C++ simulation platform, Ned Stoffel, RSoft Design - Mescal System Design Methodology, Andrew Mihal, UC Berkeley Mescal Group - Embedded S/W Development Using PTII: Modeling Extensions, Data Representation, Compilation, Zoltan Kemenczy and Sean Simmons, Research in Motion - Java Code Generation, Steve Neuendorffer, UC Berkeley Ptolemy Group - C Code Generation, Ankush Varma, Shuvra S. Bhattacharyya, University of Maryland, - JHDL Hardware Generation, Michael J. Wirthlin, Matthew Koecher, Brigham Young University - Ptolemy II and MDA, Vincent Arnould of Thales - The Ptolemy II Graph Package, Shahrooz Shahparnia, Fuat Keceli, Ming-Yung Ko,Yuhong Xiong, Jie Liu, Shuvra S. Bhattacharyya University of Maryland - The OpenModelica Project - Object-Oriented Modeling and Simulation for Continuous and Discrete-Event Systems, Peter Bunus, Peter Fritzson, Peter Aronsson, Vadim Engelson, Levon Saldamli. Linkoping University, Sweden - Embedded S/W Development Using PTII (Poster), Zoltan Kemenczy and Sean Simmons, Research in Motion - Verification of Process Networks derived from Matlab by Compaan using Ptolemy, Bart Kienhuis, Leiden University, The Netherlands - Design Space Exploration in Ptolemy, Bart Kienhuis, Leiden University, The Netherlands - Efficient and orderly co-simulation of heterogeneous computational models, Daniel Lázaro Cuadrado - Simulation to Implementation: Hardware in the Loop Simulation and Code Generation, Steve Neuendorffer, UC Berkeley Ptolemy Group - Methods for Monitoring, Benchmarking and Tuning of Ptolemy II Models' Performance, Mohamed Salem, Ellipsis Design - Using High-level Synthesis from SystemC for Architectural Exploration, John Sanguinetti, Forte Design Systems - Formal composition of web services, Xavier Warzee, Valtech Technologies/General Electric Medical Systems - JHDL Domain, Michael J. Wirthlin, Trent Vandenberghe, Brigham Young University - Image Processing in Ptolemy II, James Yeh, UC Berkeley Ptolemy Group - Distributed Ptolemy Models, Yang Zhao, Xiaojun Liu, UC Berkeley Ptolemy Group - Communications Systems Modeling in Ptolemy II, Rachel Zhou, UC Berkeley Ptolemy Group - Models of Computation in Hollywood, Chamberlain Fong, Digital Domain - Cal: An Actor Definition Language, Joern Janneck, UC Berkeley Ptolemy Group - Multiple Objetive Evolutionary Programming (MOEP), Greg Rohling, Georgia Tech - The Component Interaction Domain: Modeling Event-Driven and Demand-Driven Applications, Xiaojun Liu, Yang Zhao, UC Berkeley Ptolemy Group - TinyGALS: A Programming Model for Event-Driven Embedded Systems, Elaine Cheong, UC Berkeley Ptolemy Group - Conditional Scheduling for Giotto, Ben Horowitz, UC Berkeley Massacio Project - Plans for the Future, Edward A. Lee, UC Berkeley Ptolemy Group Personnel --------- No personnel changes. 4. Publications [1] Thomas A. Henzinger, Christoph M. Kirsch, and Slobodan Matic. Schedule carrying code. Proceedings of the Third International Conference on Embedded Software (EMSOFT), Lecture Notes in Computer Science, Springer-Verlag, 2003. [2] Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Marielle Stoelinga. The element of surprise in timed games. Proceedings of the 14th International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science, Springer-Verlag, 2003. [3] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. Proceedings of the 30th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science, Springer-Verlag, 2003. [4] Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample guided control. Proceedings of the 30th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science, Springer-Verlag, 2003. [5] Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, and Jens Palsberg. Stack size analysis for interrupt-driven programs. Proceedings of the Tenth International Static Analysis Symposium (SAS), Lecture Notes in Computer Science, Springer-Verlag, 2003. [6] Jie Liu and Edward A. Lee,"On the Causality of Mixed-Signal and Hybrid Models," 6th International Workshop on Hybrid Systems: Computation and Control (HSCC '03), April 3-5, 2003, Prague, Czech. http://ptolemy.eecs.berkeley.edu/papers/03/hybridCausality [7] Xiaojun Liu, Jie Liu, Johan Eker, and Edward A. Lee, "Heterogeneous Modeling and Design of Control Systems," Software-Enabled Control: Information Technology for Dynamical Systems, Tariq Samad and Gary Balas (eds.), Wiley-IEEE Press, April 2003. http://ptolemy.eecs.berkeley.edu/publications/papers/03/controlSys/ [8] Stephen Neuendorffer,"Implementation Issues in Hybrid Embedded Systems", Technical Memorandum No. UCB/ERL M03/22, University of California, Berkeley, CA, 94720, USA, June 24, 2003. http://ptolemy.eecs.berkeley.edu/publications/papers/03/crazyboard/ [9] S. Zelinski, T. J. Koo, and S. Sastry, "Optimization-based Formation Reconfiguration Planning For Autonomous Vehicles," in the Proceedings of International Conference on Robotics and Automation, Taipei, Taiwan, May 2003. [10] T. John Koo, S. Zelinski, and S. Sastry, "Formation Reconfiguration for Autonomous Vehicles," in the Proceedings of AHS 59th Annual Forum and Technology Display "Vertical Flight Transformations," Phoeniz, AZ, May 6-8, 2003. 5. Financial Data Provided separately on a quarterly basis by the university.