QUARTERLY PROGRESS REPORT CONTRACTOR: University of California at Berkeley AGREEMENT NUMBER: not yet assigned CONTRACT PERIOD: 9/1/99 - 12/31/03 TITLE: Software Enabled Control REPORT PERIOD: 4/1/00 - 6/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. On the formal side, we introduced a hierarchical model for the design and analysis of embedded control systems called Masaccio. This will be the basis for the next generation of the hybrid model checker Hytech. We also focused heavily on the study of games for synthesizing controllers. Our original results concern the solution of probabilistic games (for modeling synchronous control and uncertain environments) and abstraction mechanisms for games. At the PI meeting in Albaquerque, we demonstrated hierarchical heterogeneous modeling and design using Ptolemy II, with integrated smart sensors and motor-drive actuators to control small robots. We also described a preliminary implementation of a time-triggered language, and progress on its underlying formalism. On the control side, we showed that the controller synthesis problem is semi-decidable for special classes of hybrid systems where the continous vector fields are linear, and we obtained original results in the optimal control of switched linear systems. 1. Research Status Formal Modeling and Analysis ============================ We defined a hierarchical model for the design and analysis of embedded control systems called Masaccio. The next generation of Hytech is planned to operate on Masaccio models. We also focused heavily on the study of games. Games are the natural setting for studying the synthesis of controller: a controller is a winning strategy of a game system vs. control. Our original results concern the solution of probabilistic games (for modeling synchronous control and uncertain environments) and abstraction mechanisms for games. To our knowledge, our work on abstraction of games is the first attempt at an abstract interpretation theory for controller synthesis. Masaccio: a formal model for embedded components ------------------------------------------------ We defined Masaccio, a formal model for hybrid dynamical systems which are built from atomic discrete components (difference equations) and atomic continuous components (differential equations) by parallel and serial composition, arbitrarily nested. Each system component consists of an interface, which determines the possible ways of using the component, and a set of executions, which define the possible behaviors of the component in real time. The purpose of Masaccio is to enable hierarchical formal modeling and verification of hybrid systems. Concurrent omega-regular games ------------------------------ We consider two-player games which are played on a finite state space for an infinite number of rounds. The games are concurrent, that is, in each round, the two players choose their moves independently and simultaneously; the current state and the two moves determine a successor state. We consider omega-regular winning conditions on the resulting infinite state sequence. To model the independent choice of moves, both players are allowed to use randomization for selecting their moves. This gives rise to the following qualitative modes of winning, which can be studied without numerical considerations concerning probabilities: sure-win (player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure winning with probability 1), limit-win (player 1 can ensure winning with probability arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability bounded away from 0), positive-win (player 1 can ensure winning with positive probability), and exist-win (player 1 can ensure that at least one possible outcome of the game satisfies the winning condition). We provide algorithms for computing the sets of winning states for each of these winning modes. In particular, we solve concurrent Rabin-chain games in n^O(m) time, where n is the size of the game structure and m is the number of pairs in the Rabin-chain condition. While this complexity is in line with traditional turn-based games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games. This is because concurrent games violate two of the most fundamental properties of turn-based games. First, concurrent games are not determined, but rather exhibit a more general duality property which involves multiple modes of winning. Second, winning strategies for concurrent games may require infinite memory. Abstract interpretation of game properties ------------------------------------------ We apply the theory of abstract interpretation to the verification of game properties for reactive systems. Unlike properties expressed in standard temporal logics, game properties can distinguish adversarial from collaborative relationships between the processes of a concurrent program, or the components of a parallel system. We consider two-player concurrent games ---say, component vs. environment--- and specify properties of such games ---say, the component has a winning strategy to obtain a resource, no matter how the environment behaves--- in the alternating-time mu-calculus (AMU). A sound abstraction of such a game must at the same time restrict the behaviors of the component and increase the behaviors of the environment: if a less powerful component can win against a more powerful environment, then surely the original component can win against the original environment. We formalize the concrete semantics of a concurrent game in terms of controllable and uncontrollable predecessor predicates, which suffice for model checking all AMU properties by applying boolean operations and iteration. We then define the abstract semantics of a concurrent game in terms of abstractions for the controllable and uncontrollable predecessor predicates. This allows us to give general characterizations for the soundness and completeness of abstract games with respect to AMU properties. We also present a simple programming language for multi-process programs, and show how approximations of the maximal abstraction (w.r.t. AMU properties) can be obtained from the program text. We apply the theory to two practical verification examples, a communication protocol developed at the Berkeley Wireless Research Center, and a protocol converter. In the wireless protocol, both the use of a game property for specification and the use of abstraction for automatic verification were instrumental to uncover a subtle bug. 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. For example, publish-and-subscribe interactions between components (with priorities) are suitable for managing irregular events and alarms, but not so well suited for regular, high-sample-rate signal processing nor for continuous dynamics. Time-triggered formalisms are better suited for hard-real-time processing, but not as well suited for irregular interactions. Our approach, therefore, is to study the composition of these models and to build software that enables systematic composition. Another example of such heterogeneous compositions uses state machine models to govern modes of operation of systems whose behavior is better represented in some other way, such as by continuous-time models, to get hybrid systems. We are applying modern software concepts, including sophisticated approaches to concurrency management, discovery, middleware, type systems, and higher-order functions to this problem domain. We are using a pre-existing Java-based software framework called Ptolemy II as an experimental platform, and we are working with the Berkeley Aerobots project to put our software concepts on autonomous model helicopters. Fresco ------ Ben Horowitz and Christoph Meyer have finished a draft implementation of a skeleton of Giotto in VxWorks. Giotto is our evolving time-triggered implementation language. We intend the implementation to be portable between RTOSs (e.g., Real-time Linux, QNX, etc.) In particular, we have limited our use to POSIX features. We found the logic analyzer of VxWorks very helpful, both for debugging and for understanding the behavior of the RTOS. There is a screen shot available at http://www-cad.eecs.berkeley.edu/~fresco/teos/teos3-log-2.gif, which serves as a good example. In it, one can see four processes of interest: - com, which is responsible for intertask communication - task0, which executes four times per round - task1, which executes two times per round - task2, which executes once per round There is also an idle task, which is not of interest. Here's what's going on: - at time 12, the communication task begins to run. It makes task0, task1, and task2 ready to run. The heavy green horizontal line signifies that a task is running, and the sawtooth horizontal line signifies that a task is ready. - at time 22, task0 begins to run, and finishes shortly thereafter. - at time 23, task1 begins to run. It finishes at time 34. - at time 34, task2 begins to run. It gets preempted by com at time 43. - at time 50, task1 begins to run, and finishes shortly thereafter. - at time 52, task2 resumes, and finishes at time 61. - ... Note that task2 continues to run across multiple invocations of task0. This is possible because of the preemptive scheduler of VxWorks. Albuquerque Demo ---------------- At the PI meeting in Albuquerque, we demonstrated hierarchical heterogeneous modeling and design using Ptolemy II to integrate smart sensors and motor-drive actuators to control small robots. The implementation used a publish-and-subscribe fabric (JavaSpaces), a service discovery fabric (Jini), a discrete-event simulation engine (the Ptolemy II DE domain), and a dataflow computation engine (the Ptolemy II SDF domain). It showed models that were modified during execution, with thread-safe updates of static analysis information. The discovery mechanism was used to dynamically discover the publish and subscribe fabric. We believe that the same infrastructure can be used to discover other publish-and-subscribe fabrics, such as the OCP. The small robots were Lego Mindstorms, and the sensor was a tilt sensor from Telemonitor connected via an IEEE 1451.2 bus to an Agilent NCAP (network capable application processor), which hosted a web server. The robots and the sensors were abstracted as Ptolemy II actors. In the case of the robots, the actor functioned as a proxy, internally implemented by sending commands to the robot over the serial port and an infrared link. To improve reliability and directionality of the infrared link, we used a port replicator (designed and built by Win Williams) to drive two distinct infrared emitters. The Telemonitor sensors were abstracted as actors that performed HTTP queries of the NCAP to obtain sensor information and to configure the sensors. A number of issues were raised by this demo, particularly with regard to the semantics of the publish-and-subscribe infrastructure. There are a number of options in configuring this infrastructure. For instance: - Should events have time stamps? - Should these time stamps have global significance? - Should delivery of events be reliable (with retry if necessary)? - Should events always be delivered in the order they are produced? - How can we coordinate events from multiple sources? - Should synchronous event delivery be supported? - How should events from multiple publishers be merged? - How should dynamic redirection and resourcing of events be supported? - Should the fabric provide persistent state? - Should the fabric provide history services? In view of these questions, the next step is to define a precise semantics for a publish-and-subscribe fabric for software-enabled control systems. The demo builders were Chamberlain Fong, Christopher Hylands, Jie Liu, Xiaojun Liu, Steve Neuendorffer, Sonia Sachs, and Win Williams. Discovery --------- At the Albuquerque PI meeting, we also proposed the use of discovery mechanisms (such as Jini) to construct a "Meta-OCP," where various configurations of interconnection services could be delivered in a modular way. For example, a component may request a reliable stream-based delivery mechanism to get sampled data from point A to point B. The meta-OCP would respond with byte-code that implements a suitable interface, using for example TCP/IP and sockets, bypassing any central infrastructure. This might be used to transport regularly sampled data, such as audio data. In another example, a component requests a shared data repository visible to a number of components. The delivered code might interact with a Linda-style tuple space, such as that in the OCP. This might be used, for example, to read the current temperature from a sensor. In a third example, a component requests an interface to send time-stamped data that must be delivered and dealt with within some specified deadline. The delivered code might interact with TAO via the OCP. This might be used, for example, to deliver motion control data. Controller Design and Analysis ============================== We have done extensive research on hybrid system theory which enable multi-agent multi-modal control. The objective is to use hybrid system model for the design, analysis and synthesis of multi-agent multi-modal systems that deliver high levels of mission reliability in dynamic and rapidly evolving environments. For controller synthesis, we have worked on multi-modal control derivation and computations for optimal hybrid control. The objective of multi-modal control research 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. Synthesis of least restrictive controllers based on optimal control theory for classes of systems in which the reachability problem are deciable are undertaking. Modeling of hybrid systems in both deterministic and nondeterministic settings are currently being investigated. The objective of the studies is to have a deeper and border understanding of dynamical behaviors of hybrid systems in order to benefit the development of new algorithms for analysis, synthesis, verification and simulation. Component-based design technique will be deployed for the design of embedded software which enables multi-modal control. In parallel, formal modeling language, unified modeling language, is used for modeling of existing embedded software running on helicopter-based unmanned aerial vehicle developed at Berkeley to motivate the study in applying component-based design techniques for real-time embedded system. Semidecidable Controller Synthesis for Classes of Linear Hybrid Systems ----------------------------------------------------------------------- A problem of great interest in the control of hybrid systems is the design of least restrictive controllers for reachability specifications. Controller design typically uses game theoretic methods to compute the region of the state space for which there exists a control such that for all disturbances, an unsafe set is not reached. In general, the computation of the controllers requires the steady state solution of a Hamilton-Jacobi partial differential equation which is very difficult to compute, if it exists. We show that for special classes of hybrid systems where the continous vector fields are linear, the controller synthesis problem is semi-decidable: There exists a computational algorithm which, if it terminates in a finite number of steps, will exactly compute the least restrictive controller. This result is achieved by a very interesting interaction of results from mathematical logic and optimal control and presents us with the first semi-decidable controller synthesis result for such rich classes of hybrid systems. Toward Optimal Control of Switched Linear Systems ------------------------------------------------- The problem of driving the states of a switched linear control system between boundary states is investigated. We propose tight lower bounds for the minimum energy control problem. We furthermore show that the fact that the dynamics is changing discontinuously on the switching surface gives rise to phenomena that can be treated as a decidability problem for hybrid control systems, using ideas from mathematical logic. 2. Interactions and Technology Transfer - On May 2nd, 2000, we hosted a meeting to bring together the system-level design language (SLDL) efforts of VHDL International, Open Verilog International (now merged with VI), and the VSIA. At this meeting we described the domain concept as it has been evolving in this project as well as the evolving abstract syntax being developed under the aegis of the GSRC project at Berkeley. - Thomas Henzinger and Edward Lee attended the April 27 and 28 OCP meeting at the Boeing Leadership Center in St. Louis. - Thomas Henzinger attended the June 20 and 21 High Confidence Aviations Systems meeting in Alexandria, VA. - David Shim attended the June 8 and 9 Controls API meeting at the Boeing Leadership Center in St. Louis. 3. Publications [1] Jie Liu and Edward A. Lee, "Component-based Hierarchical Modeling of Systems with Continuous and Discrete Dynamics", Invited paper to the Conference on Computer-Aided Control System Design (CACSD), Anchorage, AK, September, 2000. [2] Jeff Tsay, "A Code Generation Framework for Ptolemy II," ERL Technical Report UCB/ERL No. M00/25, Dept. EECS, University of California, Berkeley, CA 94720, May 19, 2000. [3] Bilung Lee, "Specification and Design of Reactive Systems", Ph.D. thesis, Memorandum UCB/ERL M00/29, Electronics Research Laboratory, University of California, Berkeley, May, 2000. [4] Thomas A. Henzinger, "Masaccio: a formal model for embedded components," Proceedings of the First IFIP International Conference on Theoretical Computer Science (TCS 00), Lecture Notes in Computer Science 1872, Springer-Verlag, September 2000, pp. 549--563. [5] Luca de Alfaro and Thomas A. Henzinger, "Concurrent omega-regular games, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS 00), June 2000. [6] Thomas A. Henzinger, Rupak Majumdar, F.Y.C. Mang, and J.-F. Raskin, "Abstract interpretation of game properties," Proceedings of the Seventh International Static Analysis Symposium (SAS 00), Lecture Notes in Computer Science, Springer-Verlag, 2000. [7] Omid Shakernia, George J. Pappas, Shankar Sastry, "Semidecidable Controller Synthesis for Classes of Linear Hybrid Systems," submitted to 39th IEEE Conf. on Decision and Control, Sydney, AU, December 2000. [8] M. Egerstedt, P. Ogren, O. Shakernia, J. Lygeros, "Toward Optimal Control of Switched Linear Systems", submitted to 39th IEEE Conf. on Decision and Control, Sydney, AU, December 2000. 4. Financial Data Provided separately on a quarterly basis by the university.