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: 9/1/99 - 3/31/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. We extended the theory and implementation of the model checker HyTech to cope with rectangular and nonlinear hybrid systems. We also developed a systematic classification of which requirements of hybrid systems can be model checked. Finally, we started a new project, FRESCO, on faithfully implementing hybrid models in real-time software. We have done extensive experimentation with various embedded devices with sensors and actuators, integrating them in various ways into our software infrastructure. The objective is to develop techniques for portable, component-based design of embedded software. We plan to use the same techniques for programming a variety of platforms, including, eventually, the autonomous helicopters. But several simpler devices provide a safer experimentation framework. 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. 1. Research Status Formal Modeling and Analysis ============================ We extended the theory and implementation of the model checker HyTech to cope with rectangular and nonlinear hybrid systems. We also developed a systematic classification of which requirements of hybrid systems can be model checked. Finally, we started a new project, FRESCO, on faithfully implementing hybrid models in real-time software. Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods ----------------------------------------------------------------------- Since hybrid embedded systems are pervasive and often safety-critical, guarantees about their correct performance are desirable. The hybrid systems model checker HyTech provides such guarantees and has successfully verified some systems. However, HyTech severely restricts the continuous dynamics of the system being analyzed and, therefore, often forces the use of prohibitively expensive discrete and polyhedral abstractions. Ben Horowitz, Rupak Majumdar, and Howard Wong-Toi designed a new algorithm, which is capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear differential equations. The new algorithm conservatively overapproximates the reachable states of a hybrid automaton by using interval numerical methods. Interval numerical methods return sets of points that enclose the true result of numerical computation and, thus, avoid distortions due to the accumulation of round-off errors. The new algorithm is implemented in a successor tool to HyTech called HyperTech. Three examples are considered: a thermostat with delay, a two-tank water system, and an air-traffic collision avoidance protocol. HyperTech enables the direct, fully automatic analysis of these systems, which is also more accurate than the use of polyhedral abstractions. Robust Undecidability of Timed and Hybrid Systems ------------------------------------------------- The algorithmic approach to the analysis of timed and hybrid systems is fundamentally limited by undecidability, of universality in the timed case (where all continuous variables are clocks), and of emptiness in the rectangular case (which includes drifting clocks). Traditional proofs of undecidability encode a single Turing computation by a single timed trajectory. These proofs have nurtured the hope that the introduction of "fuzziness" into timed and hybrid models (in the sense that a system cannot distinguish between trajectories that are sufficiently similar) may lead to decidability. J-F Raskin showed that this is not the case, by sharpening both fundamental undecidability results. Besides the obvious blow our results deal to the algorithmic method, they also prove that the standard model of timed and hybrid systems, while not "robust" in its definition of trajectory acceptance (which is affected by tiny perturbations in the timing of events), is quite robust in its mathematical properties: the undecidability barriers are not affected by reasonable perturbations of the model. Symbolic Model Checking for Rectangular Hybrid Systems ------------------------------------------------------ An important case of hybrid systems are the rectangular automata. First, rectangular dynamics can naturally and arbitrarily closely approximate more general, nonlinear dynamics. Second, rectangular automata are the most general type of hybrid systems for which model checking --in particular, LTL model checking-- is decidable. However, on one hand, the original proofs of decidability did not suggest practical algorithms and, on the other hand, practical symbolic model-checking procedures --such as those implemented in HyTech-- were not known to terminate on rectangular automata. Rupak Majumdar remedied this unsatisfactory situation: he develope a symbolic method for LTL model checking which can be performed by HyTech and is guaranteed to terminate on all rectangular automata. This is done by proving that our method for symbolic LTL model checking terminates on an infinite-state transition system if the trace-equivalence relation of the system has finite index, which is the case for all rectangular automata. A Classification of Symbolic Transition Systems ----------------------------------------------- Rupak Majumdar defined five increasingly comprehensive classes of infinite-state systems, called STS1-5, whose state spaces have finitary structure. For four of these classes, examples from hybrid systems can be provided. STS1: These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by (1) iterating the predecessor and boolean operations starting from a finite set of observable state sets, and (2) terminating when no new state sets are generated. This enables model checking of the mu-calculus. STS2: These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive boolean operations. This enables model checking of the existential and universal fragments of the mu-calculus. STS3: These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive boolean operations (intersection is restricted to intersection with observables). This enables model checking of linear temporal logic. STS4: These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the mu-calculus. STS5: These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered. This enables model checking of reachability properties. FRESCO: Formal Real-time Software Components -------------------------------------------- We have been designing a formal, structured modeling language for hybrid control systems, called Masaccio, and a time-triggered implementation language, called Giotto. Our eventual goal is to establish requirements in Masaccio by model checking, in a way which guarantees that the Giotto implementation meets the requirements. Rupak Majumdar is implementing Giotto in Lego Mindstorms. Ben Horowitz and Christoph Meyer are implementing Giotto on 486 processors communicating by wireless Ethernet. Vinayak Prabhu is designing a case study to refine a Masaccio model for a search-and-recue mission of multiple coordinating Lego Mindstorms robots, into Giotto programs on the base station and the individual robots. Embedded Software Design ======================== We have been experimenting extensively with embedded computing devices, sensors, and actuators, to gain experience and to identify a suite of experimental platforms that are safer to experiment with than the Bear Project helicopters. The objective is to develop techniques for portable, component-based design of embedded software. We plan to use the same techniques for programming a variety of platforms, including, eventually, the autonomous helicopters. We have performed quite a few investigations, and made quite a bit of progress in understanding this space. Also, the department has committed space to an embedded systems lab as part of remodeling project on the fifth floor of Cory Hall. Jini and Java Spaces -------------------- To give us a versatile experimental platform in anticipation of the Boeing OCP, we have developed a publish-and-subscribe mechanism in Ptolemy II based on Java Spaces, a Linda-style distributed messaging system from Sun. Jie Liu and Yuhong Xiong created a demonstration where a publisher extracts stock market data from a web source and and subscriber consumes that data to generate trend plots. This demonstration shows the network integration and publish-and-subscribe interactions working with Ptolemy II. Moreover, the demo uses Jini, a networked service-discovery mechanism from Sun, intended for embedded devices. Service discovery is not currently part of the OCP plan, but we hope to develop a better understanding of its role to help determine whether it should be incorporated later, and in what form. Agilent Smart Sensors --------------------- The stock market data used by Jie and Yuhong is a metaphor for sensors and actuators providing HTTP interfaces, such as the BFOOT smart sensor family from Agilent. We have been working with Agilent, and have obtained two NCAPs (network-capable application processors) and a variety of STIMs (Smart Transducer Interface Modules, sensors and actuators that interface to the NCAP via the standard 1451.2 bus). Chamberlain Fong and Xiaojun Liu interfaced a tilt sensor to Ptolemy II using the same publish-and-subscribe mechanism used by Jie and Yuhong for the stock market example. Xiaojun demonstrated the tilt sensor controlling a Lego robot (see below). STIMs are available from Telemonitor, who makes the tilt sensor mentioned above as well as a thermocouple, Electronics Development Corporation (www.elecdev.com), which sells some evaluation kits that include an accelerometer, and Analog Devices (www.analog.com), who make a product called the MicroConverter that includes multichannel analog to digital and digital to analog converters and a microcontroller counters/timers and programmable I/O lines. Lego Mindstorms --------------- We have acquired a suite of Lego Mindstorm kits, which include a microcontroller with motor drives and a variety of sensors linked to a host via an infrared link. Win Williams created a simple coordinated control example using the visual programming environment (RCX) provided with the Legos. In this example, two robots are started, moving in parallel. When one collides with an obstacle, the robots communicate via the infrared port, and with synchronized movements, both back up and turn to avoid the obstacle. Christopher Hylands then obtained the Java Tanks example from Sun Microsystems, and Xiaojun Liu built a Ptolemy II actor that issues instructions to the Lego through the serial port of a PC. His first example generated random walk instructions from a Ptolemy II model in the synchronous-dataflow (SDF) domain. His realization, which is based on Java Tanks, uses "not-quite C" on the Legos and Java on the host. Christopher also experimented a bit with using Esterel and Lustre (two synchronous languages used for embedded control systems) for the Legos (see http://www.emn.fr/richard/lego/). Xiaojun Liu tested the range and directedness of the IR link between the infrared tower connected to the computer serial port, and the Lego robot. He found the link to be fairly unreliable, particularly with flourescent lights on. We are considering putting another single-board computer on the Legos with a wireless LAN PCMCIA card. Luca DeAlfaro experimented with using infrared sensors for range and direction detection on the Legos. Pioneer and Jini ---------------- Jie Liu and Steve Neuendorffer created a software infrastructure in Java for programming a Pioneer mobile robot borrowed from the Bear project and the Legos using the same code. This is our first serious demonstration of platform independent software development. The Pioneer is a much more substantial platform than the Legos, and has a single-board computer running Linux. Their software uses Jini to distribute code to robots, or in the case of the Legos, to a proxy for the robots running on a laptop computer. The code that is distributed is Java bytecode. When a task is needed of a robot, an instance of a Java class is posted to the Jini server, and the robots are notified. Any robot that is available and implements an interface compatible with the posted task can grab the code from the Jini server to execute the task. Robot Arm --------- Chamberlain Fong assembled from a kit a small robot arm with four degree of freedom motion and a gripper. He built a demonstration of a controller this arm that uses a new domain in Ptolemy II that he is developing, DT (discrete time). The demonstration includes an on screen animation, through which commands are entered using the keyboard, and the mouse is used for changing the viewpoint of the arm simulator. The communication between software components is mostly angles and polygons generated by a forward kinematics controller. Chamberlain is working on an inverse kinematics controller. The robot arm is connected to a host computer through the serial port. Handspring Visors ----------------- Christopher Hylands experimented with the KVM (a minimal Java virtual machine) running on Handspring Visors (handheld electronic organizers). We selected the Handspring Visor instead of the more popular Palm Pilot because the Visor includes a bus with a published interface, and thus has much more promise for use in embedded systems. Christopher was able to get a small portion of the Ptolemy II code to compile for the KVM, and was able to port a small process networks application. Christopher attempted to get the IR port on the Handspring to communicate with the Legos, but was unsuccessful. Dallas Tini ----------- We obtained a pair of Dallas Seminconductor Tini boards, small single-board computers that include a Java virtual machine in a DIMM form factor. They support a serial port, a 1-wire interface, CAN bus and 10baseT ethernet. http://www.ibutton.com/TINI/software/index.html says: "The Java VM on TINI conforms to Sun's *Embedded* Java platform, version 1.1 of the Java API. Embedded in TINI's flash memory are java.lang, java.net, java.io, java.util; there is room in RAM for other packages of your choice. Also in flash memory are com.dalsemi packages for accessing the TINI command shell slush, the 1-WireŽ bus and several system parameters." TINI implements none of the serialization, reflection, and dynamic class loader, so it is still far from RMI. That is, at this time, it is impossible to make the TINI board a Jini device and access the Java Space directly. It is doubtful that these devices would be easy to interface to the OCP, except through proxies running on a more substantial host. Nonetheless, there are interesting possibilities. Dallas makes a small memory device called an iButton. The idea is that you might carry an iButton with you (attached to a ring, or a key, or a badge) and the Tini board reads it and personalizes its environment to you. Real-Time Java -------------- Because the extensive Java infrastructure that we have built (in the form of Ptolemy II), we have been studying the various real-time Java projects with an eye towards being able to provide native Java support for the OCP, including its quality of service features. Particular realizations we have studied include Esmertec, FIXME. CORBA Sensors ------------- Brian Vogel created a demonstration that uses CORBA to obtain and plot data from an ultrasonic detector connected to a Windows NT machine running a web server. He uses the audio hardware of the PC as an analog interface to the sensor. This was our first networked sensor application, and it illustrates how smart sensors might communicate with controllers via the OCP. 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. Multi-Modal Control Derivation ------------------------------ John Koo, Shankar Sastry, and George Pappas of University of Pennsylvania have been working on mode switching synthesis for specifications which are based on mission completion properties. In particular, we are interested in reachability specifications at this point. The objective 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. We hope to implement the algorithms based on existing efficient methods for reachability computation and apply the algorithms to certain classes of dynamical systems. Component-based Design Technique for Multi-Modal Control -------------------------------------------------------- Based on previous works by Jie, Xiaojun, John Koo and Bruno Sinopoli on the implementation of a multi-modal system with fixed mode sequences as a hierarchical hybrid system in Ptolemy II, we are currently investigating the use of the proposed component-based design technique to implement a scale down version of UAV flight management system which facilitate on-line control mode sequence generation. The proposed mode switching algorithm for reachability specifications will be used to demonstrate the versatility of the proposed software design technique for the design of embedded software which enables multi-modal control. Computations for Optimal Hybrid Control --------------------------------------- Rene Vidal, Shawn Schaffert, John Lygeros and Shankar Sastry have developed algorithms for computing the maximal controlled invariant set and least restrictive controller for discrete time systems. We show that the algorithm can be encoded using quantifier elimination, which leads to a semi-deciablity result for definable system. Rene Vidal and Omid Shakernia have implemented an algorithm for a least restrictive controller synthesis based on robust semidefinite programming. Omid Shakernia has shown theoretical result on decidable controller synthesis for classes of linear systems. Modeling of Hybrid Systems ------------------------------------- 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 of hybrid systems. Jun Zhang, Karl Johansson, John Lygeros and Shankar Sastry have extended several important results of classical dynamical systems to hybrid dynamical systems, especially those with Zeno executions. Slobodan Simic, Karl Johansson, John Lygeros and Shankar Sastry have introduced a new framework for a global geometric study of hybrid systems. Its usefulness is demonstrated in analysis of the Zeno phenomenon and stability of hybrid equilibria. Ekaterina Lemch has studied the controllability of hybrid system in this geometric framework. Probabilistic Hybrid Systems ---------------------------- Fault detection and handling need to be designed so as to guarantee a hierarchical decrease in functionality from the least safety-critical to the most. Off-line, the fault handling routines need to be analyzed and verified in a probabilistic framework. Jianghai Hu, John Lygeros and Shankar Sastry have extended the deterministic framework of hybrid system to nondeterministic one. This provides an analytical framework for the verification of fault detection and handling. UAV Control Software Development -------------------------------- David Shim, Xiaojun and John Koo has been working on formal modeling of existing embedded software into Unified Modeling Language. The objective is to capture the organization of software components, scheduling scheme provided by operating systems and temporal properties and constraints of different hardware and software components. 2. Interactions and Technology Transfer We have met several times with engineers from Agilent Labs (formerly Hewlett-Packard Labs) to work on a collaboration using their BFOOT smart sensor technology. The BFOOT sensors are networked devices running HTTP servers. They include a 1451.2 standardized sensor and actuator interface. A growing number of companies are making sensors and actuators that conform to this interface. These smart sensors promise a true plug-and-play approach to construction of embedded systems. We believe (and have convinced Agilent) that our component software technology currently embodied in Ptolemy II, provides the ideal software component architecture to complement their hardware component architecture. Douglas C. Schmidt of Washington University visited us on November 10, 1999, and spent a day discussing our SEC project and the role of TAO and ACE. We attended the SEC kickoff meeting in San Francisco, October 20-22, 1999, and presented our view of models of computation and their role in the OCP. Luca de Alfaro attended the OCP working group meeting at Boeing in St. Louis in December 1999 and presented our view on orthogonalizing the concerns and formalizing the interfaces within the OCP. John Koo visited University of Pennsylvania on March 27, 2000, and presented our view of hierarchical hybrid system design methodology and its application to UAV flight management system design. Karl Johansson, Tom Henzinger and Luca De Alfaro taught a graduate course on Hybrid Systems at University of California, Berkeley, in Spring 2000. 3. Publications Magnus Egerstedt, Karl Henrik Johansson, John Lygeros, and Shankar Sastry, "Behavior based robotics using regularized hybrid automata," IEEE Conference on Decision and Control (CDC'99). Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar, and Howard Wong-Toi. Beyond HyTech: hybrid systems analysis using interval numerical methods. Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control (HSCC 2000), Lecture Notes in Computer Science, Springer-Verlag, 2000. Thomas A. Henzinger and Rupak Majumdar. Symbolic model checking for rectangular hybrid systems. Proceedings of the Sixth International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), Lecture Notes in Computer Science, Springer-Verlag, 2000. Thomas A. Henzinger and Rupak Majumdar. A classification of symbolic transition systems. Proceedings of the 17th International Conference on Theoretical Aspects of Computer Science (STACS 2000), Lecture Notes in Computer Science 1770, Springer-Verlag, 2000, pp. 13-34. Thomas A. Henzinger and J.-F. Raskin. Robust undecidability of timed and hybrid systems. Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control (HSCC 2000), Lecture Notes in Computer Science, Springer-Verlag, 2000. Karl Henrik Johansson, John Lygeros, Shankar Sastry, and Magnus Egerstedt, "Simulation of Zeno Hybrid Automata," to appear in IEEE Conference on Decision and Control (CDC'99). J. Liu, X. Liu, T.J. Koo, B. Sinopoli, S. Sastry and E.A. Lee "A Hierarchical Hybrid System Model and Its Simulation," IEEE Conference on Decision and Control, Phoenix, AZ, December 1999. John Lygeros, Karl Henrik Johansson, Shankar Sastry, and Magnus Egerstedt, "On the existence of executions of hybrid automata," to appear in IEEE Conference on Decision and Control (CDC'99). Omid Shakernia, George J. Pappas, and Shankar Sastry, "Decidable Controller Synthesis for a Class of Linear Systems," Hybrid Systems: Computation and Control(HSCC'00), Pittsburgh, PA, March, 2000. Slobodan Simic, Karl Henrik Johansson, Shankar Sastry, and John Lygeros, "Towards a Geometric Theory of Hybrid Systems," Hybrid Systems: Computation and Control (HSCC'00), Pittsburgh, PA, March, 2000. Jun Zhang, Karl Henrik Johansson, John Lygeros, and Shankar Sastry, "Dynamical systems revisited: Hybrid systems with Zeno executions", in B. Krogh and N. Lynch editors, Hybrid Systems: Computation and Control, volume 1790 of Lecture Notes in Computer Science, Springer-Verlag, New York, 2000. 4. Financial Data Provided separately on a quarterly basis by the university.