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: 10/1/02 - 12/31/02 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 solution of control problems for probabilistic systems with uncertain environments, Giotto-based and platform-based implementations of helicopter flight control systems, and formation reconfiguration planning for autonomous vehicles. 1. Research Status Formal Modeling and Analysis ============================ Time-safety checking for embedded programs ------------------------------------------ Giotto is a platform-independent language for specifying software for high-performance control applications. We developed a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We showed that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs. Trading probability for fairness -------------------------------- Behavioral properties of control systems can be formalized as objectives in two-player games. Turn-based games model asynchronous interaction between the players (the system and its environment) by interleaving their moves. Concurrent games model synchronous interaction: the players always move simultaneously. Probabilistic moves can be used to model uncertainty in the environment and failure scenarios for the system. Infinitary winning criteria (control objectives) are considered: Buchi, co-Buchi, and more general parity conditions. A generalization of determinacy for parity games to concurrent parity games demands probabilistic (mixed) strategies: either player 1 has a mixed strategy to win with probability 1 almost-sure winning), or player 2 has a mixed strategy to win with positive probability. We found efficient reductions of concurrent probabilistic Buchi and co-Buchi games to turn-based games with Buchi condition and parity winning condition with three priorities, respectively. From a theoretical point of view, the latter reduction shows that one can trade the probabilistic nature of almost-sure winning for a more general parity (fairness) condition. The reductions improve understanding of concurrent games and provide an alternative simple proof of determinacy of concurrent Buchi and co-Buchi games. From a practical point of view, the reductions turn solvers of turn-based games into solvers of concurrent probabilistic games. Thus improvements in the well-studied algorithms for the former carry over immediately to the latter. In particular, a recent improvement in the complexity of solving turn-based parity games yields an improvement in time complexity of solving concurrent probabilistic co-Buchi games from cubic to quadratic. Embedded Software Design ======================== A Giotto-based helicopter control system ---------------------------------------- We demonstrated the feasibility and benefits of Giotto-based control software development by reimplementing the autopilot system of an autonomously flying model helicopter. Giotto offers a clean separation between the platform independent concerns of software functionality and I/O timing, and the platform dependent concerns of software scheduling and execution. Functionality code such as code computing control laws can be generated automatically from Simulink models or, as in the case of this project, inherited from a legacy system. I/O timing code is generated automatically from Giotto models that specify real-time requirements such as task frequencies and actuator update rates. We extend Simulink to support the design of Giotto models, and from these models, the automatic generation of Giotto code that supervises the interaction of the functionality code with the physical environment. The Giotto compiler performs a schedulability analysis on the Giotto code, and generates timing code for the helicopter platform. The Giotto methodology guarantees the stringent hard real-time requirements of the autopilot system, and at the same time supports the automation of the software development process in a way that produces a transparent software architecture with predictable behavior and reusable components. Caltech Platform ---------------- We continue to work with Caltech on their rolling platform driven by two ducted fans. In particular, Steve Neuendorfer continues to develop code generation with the objective of providing a prototyping software environment for the platform. Caltech has debugged the PIC code for the platform, and has provided us with an instance of the board, but there hasn't been time yet to do much with it. A Ptolemy II model of 2D multi-modal helicopter example ------------------------------------------------------- John Koo contributed a 2-D multi-modal helicopter example to the Ptolemy II demo library. The model is based on T. J. Koo, S. Sastry "Output Tracking Control Design of a Helicopter Model Based on Approximate Linearization," In Proceedings of IEEE Conference on Decision and Control, Florida, December 1998. The control sequence is derived based on T. J. Koo, G. J. Pappas, and S. Sastry, "Mode Switching Synthesis for Reachability Specifications," Hybrid Systems: Computation and Control, M. D. Di Benedetto and A. Sangiovanni-Vincentelli (Eds.), Lecture Notes in Computer Science, Vol. 2034, pp. 333-346, Springer-Verlag, 2001. Controller Design and Analysis ============================== Platform-Based Embedded Software Design and System Integration for Autonomous Vehicles ------------------------------------------------------------------ Automatic control systems typically incorporate legacy code and components that were originally designed to operate independently. Furthermore, they operate under stringent safety and timing constraints. Current design strategies deal with these requirements and characteristics with ad hoc approaches. In particular, when designing control laws, implementation constraints are often ignored or cursorily estimated. Indeed, costly redesigns are needed after a prototype of the control system is built due to missed timing constraints and subtle transient errors. T. J. Koo, J. Liebman, C. Ma, B. Horowitz, A. Sangiovanni-Vincentelli, and S. Sastry 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. We illustrated our strategy by describing the (successful) application of the methodology to the design of a time-based control system for a helicopter-based Uninhabited Aerial Vehicle (UAV) so the the following objectives can be met: a. 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. b. 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. c. Our platform-based design achieves a high degree of modularity. For example, to substitute a different sensor suite in our first redesign requires only changes to the data processor and the data formatting library. The data processor would require a different sensor initialization routine and a new circular buffer; the formatting library would need a new format conversion routine. However, no part of the controller application would need to be changed. Optimization-based Formation Reconfiguration Planning For Autonomous Vehicles -------------------------------------------------------------------- Given a group of autonomous vehicles, an initial configuration, a final configuration, a set of inter- and intra- vehicle constraints, and a time for reconfiguration, the Formation Reconfiguration Planning problem is focused on determining a nominal input trajectory for each vehicle such that the group can start from the initial configuration and reach its final configuration at the specified time while satisfying the set of inter- and intra- vehicle constraints. S. Zelinski, T. J. Koo, and S. Sastry were interested in solving the Formation Reconfiguration Planning problem for a specific class of systems and a particular form of input signals so that the problem can be reformulated as an optimization problem which can be solved more efficiently, especially for a large group of vehicles. Optimization has proved to be a successful solution to the FRP problem. Our method of implementation is general and portable allowing for use in a wide range of applications for coordinated robots. For example, our method could easily be transported to two dimensions for ground robot coordination. This centralized control scheme has limitations in applications where formations are very large or communication is disrupted. For such applications, a decentralized control scheme is preferred. We are currently working on a decentralized approach to the FRP problem where each vehicle produces its own localized solution based on only local sensor information about its neighboring vehicles. As expected, this is proving to be a more complex problem. Therefore, centralized control is preferred in applications for smaller fully connected formations. 2. Interactions and Technology Transfer Presentations ------------- * Integrated Safety Envelopes; Built-in Restrictions of Navigable Airspace, Edward A. Lee, Sept. 19-20, 2002, NSF/OSTP Workshop on Information Technology Research for Critical Infrastructure Protection, Lansdowne, VA. * Demonstration of modeling and design of hybrid control systems using Ptolemy II, SEC PI meeting, Nov. 7, 2002, by Xiaojun Liu. Ptolemy II supports the heterogeneous modeling, simulation, and design of concurrent systems. The demonstration included the simulation of a multi-modal controller of a model helicopter, blending controllers that smooth transitions from one control mode to another, and heterogeneous control system simulation. * Platform-Based Embedded Software Design for Multi-Vehicle Multi-Modal Embedded Software was presented by T. J. Koo at the International Workshop on Embedded Software, Grenoble, France, October 2002. * R. Majumdar, Time-safety checking for embedded programs, EMSOFT 2002. * M. Sanvido, A Giotto-based helicopter control system, EMSOFT 2002. * C. Kirsch, Principles of real-time programming, invited talk, EMSOFT 2002. Interactions ------------ * Cedric Ma, who has been working on the SEC Project during his mater study at Berkeley, now joins Northrop Grumman Corporation as an engineer in the Vehicle Systems Division of the Integrated Systems Sector. * T. John Koo visited Northrop Grumman Air Combat Systems, El Segundo, California on Oct 21, 2002, for the NGC subcontract on High Confidence Control Design for UAVs. Technology Transfer ------------------- * A Simulink model of a helicopter control system developed by T. John Koo is distributed to Northrop Grumman for the development of High Confidence Control Design for UAVs. The model, includes vehicle dynamics, controllers, sensor models, and a kalman filter for INS/GPS Integration. Personnel --------- No personnel changes. 4. Publications [1] Jie Liu and Edward A. Lee, "On The Causality Of Mixed-signal And Hybrid Models," accepted to HSCC '03: Hybrid Systems: Computation and Control, Prague, The Czech Republic, April 3-5, 2003. [2] Elaine Cheong, Judy Liebman, Jie Liu, and Feng Zhao, "TinyGALS: A Programming Model for Event-Driven Embedded Systems," to appear in Proceedings of the 18th Annual ACM Symposium on Applied Computing (SAC'03), Melbourne, FL, Mar. 9-12, 2003. [3] B. Horowitz, J. Liebman, C. Ma, T. J. Koo, A. Sangiovanni-Vincentelli, S. Sastry, "Platform-Based Embedded Software Design and System Integration for Autonomous Vehicles," The Proceedings of the IEEE, October 2002. [4] T. J. Koo, J. Liebman, C. Ma, B. Horowitz, A. Sangiovanni-Vincentelli, and S. Sastry, "Platform-Based Embedded Software Design for Multi-Vehicle Multi-Modal Embedded Software," Embedded Software, Alberto Sangiovanni-Vincentelli and Joseph Sifakis (Eds.), Lecture Notes in Computer Science, Springer-Verlag, 2002. [5] S. Zelinski, T. J. Koo, and S. Sastry, "Optimization-based Formation Reconfiguration Planning For Autonomous Vehicles," in Proceedings of International Conference on Robotics and Automation, Taipei, Taiwan, May 2003. [6] Thomas A. Henzinger, Christoph M. Kirsch, Rupak Majumdar, and Slobodan Matic. Time-safety checking for embedded programs. Proceedings of the Second International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2491, Springer-Verlag, 2002, pp. 76-92. [7] Christoph M. Kirsch, Marco A.A. Sanvido, Thomas A. Henzinger, and Wolfgang Pree. A Giotto-based helicopter control system. Proceedings of the Second International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2491, Springer-Verlag, 2002, pp. 46-60. [8] Marcin Jurdzinski, Orna Kupferman, and Thomas A. Henzinger. Trading probability for fairness. Proceedings of the International Conference for Computer Science Logic (CSL), Lecture Notes in Computer Science 2471, Springer-Verlag, 2002, pp. 292-305. 5. Financial Data Provided separately on a quarterly basis by the university.