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/01 - 12/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: design of the embedded machine for verifying, compiling, and executing real-time code; definition, analysis, and implementation of precise reactions and responsible frameworks for heterogeneous modeling; platform-based embedded software design and system integration for a rotorcraft UAV. We have also organized the First International Workshop on Embedded Software (EMSOFT), a pilot event for a new annual conference series. 1. Research Status Formal Modeling and Analysis ============================ Some Lessons from the HyTech Experience [5] --------------------------------------- We wrote an overview of the current status of the tool HyTech, and reflected on some of the lessons learned from our experiences with the tool. HyTech is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We described some recent experiences analyzing three hybrid systems. We pointed out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluates these extensions, and arrived at some desiderata for verification tools for hybrid systems. Giotto: a time-triggered language for embedded programming [7] ---------------------------------------------------------- Giotto provides an abstract programmer's model for the implementation of embedded control systems with hard real-time constraints. A typical control application consists of periodic software tasks together with a mode switching logic for enabling and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations, and mode switches independent of any implementation platform. Giotto can be annotated with platform constraints such as task-to-host mappings, and task and communication schedules. The annotations are directives for the Giotto compiler, but they do not alter the functionality and timing of a Giotto program. By separating the platform-independent from the platform-dependent concerns, Giotto enables a great deal of flexibility in choosing control platforms as well as a great deal of automation in the validation and synthesis of control software. The time-triggered nature of Giotto achieves timing predictability, which makes Giotto particularly suitable for safety-critical applications. In the current quarter, we refined the Giotto compiler (see www.eecs.berkeley.edu/~fresco/giotto) and two Giotto based helicopter control system implementations. The ETH Zurich helicopter was described in the previous report; the Berkeley helicopter is described below [4]. The new Giotto compiler is based on the embedded machine [9]. Marius Minea defined a formal embedding of Giotto into hybrid automata, which enables the formal verification of Giotto programs. The Embedded Machine: Predictable, Portable Real-time Code [9] ---------------------------------------------------------- The Embedded Machine is a virtual machine that mediates in real time the interaction between physical processes and software processes. It separates the platform-independent from the platform-dependent issues in the compilation of embedded programs. The platform-independent compiler phase produces conventional (C) code for application tasks, and embedded-machine code that supervises the execution of the application tasks relative to external events, such as clock ticks and sensor interrupts. This code is portable and exhibits, given an input behavior, predictable (i.e., deterministic) timing and output behavior. The second, platform-dependent compiler phase checks the time safety of the code, i.e., whether platform performance and utilization enable its timely execution. We have used a prototype of the Embedded Machine to compile, verify, and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter. A robust time-safety checker and run-time system is currently being implemented. Embedded Software Design ======================== Responsible Frameworks for Heterogeneous Modeling and Design of Embedded ------------------------------------------------------------------------ Systems [1] ------- Jie Liu has completed his PhD thesis, entitled "Responsible Frameworks for Heterogeneous Modeling and Design of Embedded Systems." This dissertation studies modelling and design frameworks for heterogeneous embedded systems. Heterogeneity, in the sense that components in a system have diverse interaction styles, complicates embedded system design and challenges understandability, composability, and scalability of models. Hierarchical heterogeneous modeling approaches tame the design complexity by hierarchically composing semantically different modeling frameworks. Frameworks are software architectures that define component ontology and interaction styles. Formal frameworks for embedded software make programming models and software architectures reusable. Embedded systems that engage the real world need to be reactive. Jie's dissertation focuses on studying reactivity and its composition in different frameworks. It introduces the reactor model as an abstract operational semantics to capture interactions among components and frameworks. Within a framework, a component execution is a precise reaction if all the prerequisites for the reaction are satisfied before it is being triggered. A framework that only triggers precise reactions is a responsible framework. Precise reactions and responsible frameworks allow us to capture compositionality of reactions, answering questions such as how a composition of a framework and components can treated as an atomic component at a higher level. This compositionality is key for hierarchically composing heterogeneous models. Precise reactions and responsible frameworks are discussed in Jie's thesis for timed models. Having a notion of time helps designers define timely reactions. But it also brings challenges to timed frameworks to precisely determine the triggering time. In terms of modeling mixed-signal and hybrid systems, the challenge is how to precisely control the progression of modeling time. We present techniques for a responsible continuous-time framework to have compositional precise reactivity. These techniques involve optimistic look-ahead execution and possible rollback. Jie's thesis further studies precise reaction and responsible frameworks for priority-based run-time embedded software. A timed multitasking (TM) model of computation is proposed for programming reactive real-time embedded software. This model brings time determinism to the programming model level. He sketches a responsible run-time system that preserves the timing semantics of TM models. A reusable and platform-independent framework for distributed control --------------------------------------------------------------------- systems [6] ------- We worked out a concept for integrating the embedded programming methodology Giotto and the object-oriented AOCS Framework to create an environment for the rapid development of distributed software for safety-critical embedded control systems with hard real-time requirements of the kind typically found in aerospace applications. Giotto is middleware that offers a tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPU's, and networks. Giotto enables the decoupling of software design (functionality and timing) from implementation concerns (scheduling, communication, and mapping). It thus allows developers to concentrate on the design of the software architecture and on the implementation of the control and management functionalities required by the target application. Giotto is based on a time-triggered programming language. This ensures timing predictability and makes it particularly suitable for safety-critical applications with hard real-time constraints. Avionics systems are one of its natural target applications. The AOCS Framework is an object-oriented software framework for embedded control systems. Software frameworks are a software reuse technology. They consist of collections of components with predefined connections that capture an architectural design optimized for a specific domain. They predefine the composition and interaction of the components of a system while at the same time allowing for customization by providing hooks where default behavior can be overridden. Frameworks differ from other reuse technologies, because they make architectural as opposed to code reuse possible, and because they rely on object composition and inheritance as functionality-extending mechanisms. The AOCS Framework was developed for the European Space Agency for satellite control systems but is suitable more generally for embedded control applications. Giotto and the AOCS Framework are complementary technologies. The former addresses the real-time and physical realization concerns of an embedded system (timing, scheduling, communication, and mapping) while the latter addresses data structuring and task functionality concerns. The work described here arises from an attempt to integrate the two technologies to create an environment where real-time embedded control applications, because of the AOCS Framework, can be rapidly instantiated and, because of Giotto, are predictable in their timing properties even when distributed over multiple CPUs. The key to this integration is the delegate object mechanism, which allows software components to interact as if they reside within the same address space even when they are located in different processes or on different CPUs. The fiction of a global address space is maintained by copying entire objects between CPUs in a way that guarantees consistency and timeliness. The delegate object mechanism is innovative because, unlike rival proxy-based approaches such as CORBA or DCOM, it is specifically designed to promote timing predictability and is therefore ideally suited for hard real-time applications. While proxies ensure only referential transparency (for the user, there is no logical difference between local and remote object access, but there may be a time difference), delegate objects ensure both referential and time-bound transparency (for the user, there is neither a logical nor a time difference between local and remote object access). The on-time availability of consistent delegate objects is not achieved dynamically, on demand, but scheduled statically by the Giotto compiler, which performs a global task and communication scheduling analysis. Controller Design and Analysis ============================== Hierarchical System Architecture For Single-Agent Multi-Modal Systems --------------------------------------------------------------------- T. John Koo and Shankar Sastry presented a hierarchical system architecture for single-agent multi-modal systems. The layered system is designed to promote proof obligations so that system specification at one level of granularity conforms with that at another level and vice versa. The design principle for the construction of the hierarchy is based on bisimulation with respect to reachability specifications. Therefore, a higher-level system and a lower-level system are bisimilar. The approach is illustrated by designing a system architecture for controlling an autonomous agent. 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). Embedded Software Design and System Integration for Rotorcraft -------------------------------------------------------------- UAV Using Platforms [4] ------------------- Benjamin Horowitz, Judith Liebman, Cedric Ma, T. John Koo, Thomas A. Henzinger, Alberto Sangiovanni-Vincentelli, and Shankar Sastry presented a platform-based design approach for automatic control systems. Automation 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. In this paper, we use the concepts of platform-based design to develop a methodology for the design of automation control systems that builds in modularity and correct-by-construction procedures. We illustrate our strategy by describing the (successful) application of the methodology to the design of a time-based control system for a rotorcraft based unmanned aerial vehicle. 2. Interactions and Technology Transfer Presentations ------------- * John Koo, "Hierarchical Approach for Design of Multi-Vehicle Multi-Modal Embedded Software," Embedded Software Seminar, University of California at Berkeley, October 2, 2001. * Christoph Kirsch, "Embedded Programming with Giottoc 0.1," Embedded Software Seminar, University of California at Berkeley, October 16, 2001. * Tom Henzinger, "Interface Theories for Component-based Design," Embedded Software Seminar, University of California at Berkeley, November 6, 2001. * John Koo, "Hierarchical Approach for Design of Multi-Vehicle Multi-Modal Embedded Software," EMSOFT 2001: First Workshop on Embedded Software, Lake Tahoe, CA, October, 2001. * John Koo, "Hierarchical System Architecture for Multi-Agent Multi-Modal Systems," IEEE Conference on Decision and Control, Orlando, FL, December 2001. * John Koo, G. J. Pappas, and S. Sastry, "Multi-Modal Control of Systems with Constraints," IEEE Conference on Decision and Control, Orlando, FL, December 2001. * Tom Henzinger, "Giotto: A Time-triggered Language for Embedded Programming," First International Workshop on Embedded Software (EMSOFT 01), Tahoe City, California (October 2001). Interactions ------------ * John Rushby, Computer Science Laboratory, SRI International, "Assurance for Dependable Systems (From Refutation to Verification to Certification)," Embedded Software Seminar, 10/23/01. * We have had a number of discussions with Caltech about targetting their ducted fan rolling platform in our code generation efforts. Caltech has offered to produce a clone of the new version of their platform, due in 1Q '02 (calendar). * We have also had a number of discussions with Gary Balas of Minnesota about realizing versions of his mode-switching controller strategy in Ptolemy II. The principal objective would be to accurately model non-idealized software timing. * Tom Henzinger and Christoph Kirsch organized the First International Workshop on Embedded Software (EMSOFT 01), Tahoe City, California (October 2001). Tom Henzinger and Edward Lee are founding members of the steering committee of this new annual event. The meeting included an industrial and an academic panel on embedded software. Industrial panelists: John Fogelin (Windriver) Bill Mark (SRI) Grant Martin (Cadence) Augusto de Oliveira (Philips) Eric Verhulst (Eonic) Kees Vissers (Trimedia) Jon Ward (Honeywell) Academic panel ("The research community in embedded software--how are we organized? how should we be?"): G. Berry (Esterel Technologies), H. Kopetz (TTTech), E. Lee (Berkeley), R. Rajkumar (CMU), A. Sangiovanni-Vincentelli (Berkeley), J. Sifakis (VERIMAG), and J. Sztipanovits (Vanderbilt). Technology Transfer ------------------- * The Giotto toolset was used by embedded software and control courses at ETH Zurich (Switzerland) and at the University of Kiel (Germany) in the fall of 2001. Personnel --------- * Adam Cataldo joined the project to work on the softwalls application. * Jie Liu finished his PhD and went to work at Xerox Parc. 4. Publications [1] Jie Liu, "Responsible Frameworks for Heterogeneous Modeling and Design of Embedded Systems, "Ph.D. thesis, Technical Memorandum UCB/ERL M01/41, University of California, Berkeley, CA 94720, December 2001. [2] T. J. Koo, S. Sastry, "Bisimulation Based Hierarchical System Architecture for Single-Agent Multi-Modal Systems," to appear in Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Springer-Verlag, 2002. [3] T. J. Koo, G. J. Pappas, and S. Sastry, "Multi-Modal Control of Constrained Nonlinear Systems," to appear in Software-Enabled Control: Information Technology for Dynamical Systems," Tariq Samad and Gary Balas (Eds.), IEEE Press, 2002. [4] B. Horowitz, J. Liebman, C. Ma, R. Tal, T. J. Koo, T. A. Henzinger, and S. S. Sastry, "Hardware-in-the-loop (HIL) Simulation of Multi-Vehicle Multi-Modal Embedded Systems," to appear at IFAC World Congress on Automatic Control, Barcelona, Spain, 2002. [5] Thomas A. Henzinger, Jorg Preussig, Howard Wong-Toi, "Some Lessons from the HyTech Experience," Proceedings of the 40th Annual Conference on Decision and Control (CDC), IEEE Press, December 2001, pp. 2887-2892. [6] Timothy Brown, Alessandro Pasetti, Wolfgang Pree, Thomas A. Henzinger, Christoph M. Kirsch, "A reusable and platform-independent framework for distributed control systems," Proceedings of the 20th Annual IEEE/AIAA Digital Avionics Systems Conference (DASC), vol. 2, IEEE Press, October 2001, pp. 1-11. [7] Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch, "Giotto: a time-triggered language for embedded programming," Proceedings of the First International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2211, Springer-Verlag, 2001, pp. 166-184. [8] Thomas A. Henzinger, Christoph M. Kirsch, eds., "Embedded Software: Proceedings of the First International Workshop," Lecture Notes in Computer Science, Springer-Verlag, 2001. [9] Thomas A. Henzinger, Christoph M. Kirsch, "The Embedded Machine: predictable, portable real-time code," to appear in the Proceedings of the Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2002. 5. Financial Data Provided separately on a quarterly basis by the university.