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: 1/1/01 - 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. This reporting period had several major events. First, we held the fourth annual Ptolemy Miniconference at the Claremont Hotel. It drew 93 attendees from around the world. Second, we released version 1.0 of Ptolemy II on CD and on the web. Third, we have created an "RTOS" domain in Ptolemy II that begins concretely exploring the OCP semantics. Fourth, we have implemented single-CPU Giotto on VxWorks and are currently porting helicopter flight control to this platform. Fourth, we have made significant progress in solving hybrid pursuit-evasion games. These are described in more detail below. Ptolemy II 1.0 Release ====================== Some of the SEC work in this project depends on and extends the Ptolemy II software framework. We released versions 1.0beta, 1.0, and 1.0.1 of Ptolemy II on CD and on the web. The release notes are appended in appendix A. This release includes a new version of our working design document, which has grown to about 400 pages and thoroughly documents the software architecture. The release size is about 60Mb, of which more than half is documentation. We have had interactions with a number of users of these releases worldwide, some of whom have created quite sophisticated models. Ptolemy Miniconference ====================== We held the 4-th Biennial Ptolemy Miniconference at the Claremont Hotel on March 22 and 23, and drew 93 people. We had 24 talks and 16 posters, with over half of the presentations and posters coming from outside Berkeley. We gave a tutorial on Ptolemy II on Friday afternoon for approximately 40 of the participants. Details can be found at: http://ptolemy.eecs.berkeley.edu/ptconf The attending organizations included: - 3S Engineering, - Aalborg University, - Advantest Laboratories, - Agile Design, - Agilent Technologies, - Altera, - BAE Systems, - Berkeley Design Technology, - Brigham Young University, - Berkeley's BWRC, - Cadence Design Systems, - Chameleon Systems, - Corning Incorporated, - Univ. of Torino, - Ellipsis Digital Systems, - Emmeskay, - Ford Research Laboratory, - Georgia Institute of Technology, - GlobeSpan, - IBM T.J. Watson, - Isochip, - Laboratoire des Images et des Signaux, - Landmark Graphics, - Leiden Institute of Advanced Computer Science, - LIACS, Leiden University, - Philips Laboratories, - Radioplan GmbH, - Raytheon, - Research in Motion Limited, - SAIC, - Seoul National University, - Synopsys, - Telcordia Technologies, - Thales, - The University of Texas at Austin, - Trimedia, - University of Maryland, - University of São Paulo, - University of Southern California, - University of Texas at Austin, - Vanderbilt University, - Virtual Photonics The program included invited speakers from organizations worldwide, plus members of the Ptolemy project describing current research at Berkeley. Topics included: Models of Computation Ptolemy II Software Architecture Hybrid and Modal Modeling Code Generation MoML - Modeling Markup Language Modeling Concurrency Ptolemy II Type System ePtolemy - Distributed Modeling Control Flow Modeling Modeling of Wireless Networks Modeling Optical Networks Implementing Radar and Sonar Systems Dataflow modeling EDA/Instrument integration Process Networks from Matlab code Distributed Optimization Distributed Synchronized Clocks Debugging Ptolemy Applications Software Practice GSRC Semantics Project Friday afternoon, March 23, was devoted to a tutorial on Ptolemy II, which covered: Using and extending the GUI Overview of the actor libraries Overview of the domains How to write actors How to write applets 1. Research Status Formal Modeling and Analysis ============================ Precise Reactions ----------------- Jie Liu, Xiaojun Liu, and Yuhong Xiong have made some progress formalizing the problem of hierarchical heterogeneous precise reactions. They define precise reactions in a timed and untimed context. In both cases, an actor is modeled as a 2-level hierarchical state machine. At the high level, the state machine realizes the executable interface of Ptolemy II, which provides a set of "action methods" such as fire() and postfire(). The abstract semantics of Ptolemy II makes some assumptions about these methods. For example, the fire() method is assumed to not alter the state of a component, so it can be repeatedly invoked an indeterminate number of times in a given reaction. The postfire() method is invoked exactly once per reaction, and is allowed to commit the state updates of the component. Jie's automata formalize this notion. An actor is a sequence of (possibly infinite) states. From each state, there is a "fire" transition that loops to itself, and a "postfire" transition that goes to the next state. Each of the states at the high level can refine hierarchically to a detailed state machine. These state machines model the interaction with the outside, particularly the interaction with receivers, which implement domain semantics. This interaction results in compositions of state machines. Domain semantics are also affect by directors. Jie Liu speculates that all we need is a fairness assumption from directors. Thus, any automaton that invokes actors fairly serves as an abstract model for directors. In each round of the execution, an actor executes its automaton (composed with the receivers) as far as it can until it either blocked on receivers, or reaches the "endFire" state. The end of the fire() of the composite actor is a fixed point of this execution. Now we can define a precise reaction. If this fixed point exists, then the composite actor has a precise reaction, and that reaction is execution to this fixed point. If the execution of all automata in a composite actor can be modeled as a complete lattice, then a fixed point always exists. This framework can be used, therefore, to determine the conditions on a director, on receivers, and on actors such that precise reactions are always possible. Hierarchical Hybrid Systems and Assume-Guarantee Reasoning ---------------------------------------------------------- Marius Minea and Vinayak Prabhu have extended the assume-guarantee method for decomposing verification tasks to deal with hierarchical hybrid designs, which contain both discrete-time and continuous-time components at varying levels of granularity. The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for decomposing a verification task about a system into subtasks about the individual components of the system. The key to assume-guarantee reasoning is to consider each component not in isolation, but in conjunction with assumptions about the context of the component. Assume-guarantee principles are known for purely concurrent contexts, which constrain the input data of a component, as well as for purely sequential contexts, which constrain the entry configurations of a component. We present a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embedded software systems which interact with real-world environments. Using an example of two cooperating robots, we show refinement between a high-level model which specifies continuous timing constraints and an implementation which relies on discrete sampling. Embedded Software Design ======================== Open Control Platform --------------------- January 9-11, Brian Mendel and David Corman visited our group for an intensive planning session on the OCP. Here is a summary of the results from this meeting: 1) Boeing is going to use MoML as their XML syntax for the front end for their tool, rather than the ad hoc ASCII syntax they currently use. This will enable using Vergil (the Ptolemy II visual editor) instead of Simulink in the controls API. Simulink is difficult to work with in this context for two reasons. First, it does not have the publish and subscribe semantics of the OCP, and thus cannot provide a simulation framework compatible with the OCP. Moreover, for users familiar with Simulink semantics, using it for designs based on the OCP will be confusing because the OCP semantics will be unexpected. Second, Simulink is not an open architecture. It is difficult, for example, to attach to components customized annotations for their real-time properties, as required by the OCP. For this reason, the first version of the controls API from Boeing has a separate user interface for specifying the component properties. Moreover, there is no mechanism in Simulink for associating the functional code for a component with the icons in the graphical editor. Thus, the controls API generates template C++ files that must be manually filled in by the programmer. We are propsing that Ptolemy II be used to experiment with a better controls API. In particular, the Vergil editor could be used much the way Simulink is being used now, with the exception that annotations of real-time properties are easily done. The persistent file format is an XML schema called MoML; Boeing can interface to this XML schema to obtain a measure of software isolation. More interesting, however, would be to generate C++ code for the components, eliminating the step of creating the C++ template files and then filling them in by hand. 2) We created (Thursday morning) an initial prototype of a Ptolemy II domain that has the semantics of the OCP. We call it the RTOS domain, since it's essentially RTOS semantics, although with a twist: instead of managing process scheduling, it manages the scheduling of atomic computations that are reactions to events. We will continue with this domain and write up a description of the semantics, which Boeing will then compare against what they currently have for OCP and what they hope to have. The objective here is to experiment easily with alternative semantic models, and to be able to precisely define the semantics. More about this domain is given below. 3) Boeing raised the question of how to manage mode changes in a multi-threaded environment (the "precise mode change problem"), to which we proposed a partial solution (the atomic computations mentioned above are a key part of this solution). But it's only a partial solution, since the question still remains how these atomic computations should interact with more heavyweight computations that might be running in a separate process or thread. We can use Ptolemy II to explore the issues here. More about this below. 4) We agreed that probably David Shim should not be trying to run the OCP directly as it currently stands on his helicopters, but rather should be doing his designs through the controls API. The controls API is quite immature, however, so we suggest that David should work with us on trying to build a model first, using our Ptolemy II prototype, and then use the MoML interface to the OCP to create the implementation. RTOS Domain ----------- With input from Boeing, Jie Liu created a new domain, RTOS, that is the starting point for something that implements essentially an RTOS priority-based scheduler. It is based on the discrete-event domain, which contains an efficient implementation of a priority queue. It uses the DE scheduler where instead of time stamps we use priorities. The main objective of this domain is to explore how the precise mode change problem (see above) can be solved in the context of a priority-driven multitasking system. The basic assumption of the domain is one of an "atomic execution" interface to every component. That is, the interactions that components can have with one another and with events arriving from sensors or from the network occur entirely within procedure calls that cannot be preempted. Although the work of the component may be done in a preemptable background process, scheduled according to the control of a real-time OS, that background process operates in its own memory space and does not directly issue or receive events. Instead, the process interacts with an atomic execution facade. The RTOS domain is designed to use pre-existing domain-polymorphic actors, thus benefiting from the growing component library in Ptolemy II. Its model of time, however, is tied to real time, which raised some interesting issues that may affect either the design of the domain or the design of the domain-polymorphic actors. 1) The Clock actor, as written, does not work in the first version of this domain. The actor is designed to be able to be fired at any time. It then produces the appropriate output depending on the current time. When it reaches a transition, it calls the fireAt() method of the director to schedule the next transition. In all previous timed domains, this ensures that the actor is invoked at the time of the next transition. However, it has to detect based on current time whether to call fireAt() to schedule a future firing. But in RTOS, current time can be anything, if things get delayed enough, so the clock can never tell reliably whether to run. In our first implementation, we got the puzzling behavior that the Clock actor would sometimes stop producing outputs at random times. We have fixed this problem by creating a SequentialClock actor that expects to be invoked only at times corresponding to its events. This actor can be used anywhere that we currently use the Clock actor, except in the CT (continuous time) domain. 2) When an actor calls fireAt(), it needs to realize that the firing may be done immediately, even before fireAt() returns. The Clock actor was doing: public void initialize() { ... fireAt(sometime); initialization of local variables; } Thus, the first iteration was occurring before local variables were getting initialized. 3) The RTOS Director needs to synchronize to invoke actors because fireAt(), which uses a timer, iterates the actors in a new thread. That iteration may collide with one that is already running. There are a number of other interesting features of this semantic model, which we are further exploring. They may lead to a radical redesign of this domain. Furuta Pendulum Example ----------------------- Johan Eker, a new postdoc, created a Ptolemy II model for a Furuta pendulum, which is a particular style of inverted pendulum where the pendulum is swung on the end of an arm that is driven in a circular motion by a motor. The model has three modes, modeled using the FSM domain. The first mode is the "swing up" mode, where the control law imparts energy to the pendulum in order to swing it into the vertical position. The second mode is the "capture" mode, where the control law attempts to capture the pendulum in a vertical position. The third mode is the "stabilize" mode, where the control law attempts to hold the pendulum still in the vertical position. Each control law is implemented in the SDF (synchronous dataflow) domain, suitable for embedded software synthesis. The dynamics of the pendulum are modeled using the CT (continuous time) domain, and in particular, using the nonlinear dynamics generator that Jie Liu built for this domain. This generator takes differential equations and synthesizes a model. Finally, Johan used the GR domain (graphics) to create a 3-D animation of the simulation. This exercise was very useful. First, it showed that someone new to Ptolemy could create nontrivial models that mix multiple domains (four of them) in a short time. Second, it exposed some rough edges that have since been fixed (see below). Continuous-Time Domain ---------------------- Jie Liu has made some significant improvements to the continuous-time (CT) domain in Ptolemy II. He is now using a common scheduling infrastructure for domains that have statically calculated schedules, and he addressed some issues raised by Johan Eker in the construction of the inverted pendulum example (see above). The CT domain now has a better support for sequence actors with discrete domains inside it. Giotto ------ Driven by implementation on Lego Mindstorms and Wind River VxWorks, and by application in coordinating robots, inverted pendulum control, and helicopter flight control, the Giotto methodology underwent some significant revisions and improvements. Our current goal is to have a helicopter fly on Giotto by the end of the summer. Embedded software development for control applications consists of two phases: first modeling, then implementation. Modeling control applications is usually done by control engineers with support from tools such as Matlab or MatrixX. On the other hand, implementing control designs is a sub-discipline of software engineering. Control designs impose hard real-time requirements, which software engineers traditionally meet by tightly coupling model, code, and platform. We advocate a decoupling of these domains. The key to automating embedded software development is to understand the interface between platform-independent and platform-dependent issues. Such an interface ---i.e., an abstract programmer's model for embedded systems--- enables decoupling software design from implementation, even for distributed platforms and even in the presence of hard real-time requirements. Giotto provides an abstract programmer's model based on the time-triggered paradigm. In a time-triggered system, computational activity is triggered by the tick of a notional global clock. A time-triggered system samples its environment and coordinates communication with respect to such a clock. The time-triggered architecture (TTA) [Kopetz] is an important hardware and protocol realization of the time-triggered paradigm. The TTA has recently gained momentum in safety-critical automotive applications, where timing predictability is essential. Giotto offers the predictability of time-triggered systems, but at a higher and platform-independent level. Thus, Giotto enables the specification and automated generation of timing-predictable code for multiple, even distributed, platforms. The two central ingredients of Giotto are periodic task invocations and time-triggered mode switches. More precisely, a Giotto program specifies a set of modes. Each mode determines a set of tasks and a set of mode switches. At every time instant, the program execution is in one specific mode, say, M. Each task of M has a real-time frequency and is invoked at this frequency as long as the mode M remains unchanged. Each mode switch of M has a real-time frequency, a predicate that is evaluated at this frequency, and a target mode, say, N: if the predicate evaluates to true, then the new mode is N. In the new mode, some tasks may be removed, and others added. Giotto has a formal semantics that specifies the meaning of mode switches, of intertask communication, and of communication with the program environment. We have implemented Giotto on Lego Mindstorms (Christoph Kirsch) and on single-CPU Wind River VxWorks (Ben Horowitz). In Lego Giotto, we controlled and coordinated multiple robots in leader-follower games. In VxWorks Giotto, we controlled an inverted pendulum and we are currently porting helicopter flight control software. These applications led us to redesign Giotto in significant ways. Most importantly was the addition of so-called drivers, which are synchronous functions, to Giotto, for reading from sensor ports and writing to actuator ports. Embedded Sofware Course ----------------------- Christoph Kirsch (postdoc in Tom Henzinger's group) is teaching a graduate seminar course on embedded software this semester. Title: Embedded Software Engineering Brief Overview: This 3 unit course will provide an introduction to embedded software engineering which is a young research discipline on design methodologies for embedded software development. The course begins with an introduction to real-time operating system concepts and real-time communication protocols. Techniques like rate-monotonic scheduling and earliest deadline first as well as real-time protocols like TTP and CAN will be illustrated. The second half of the course emphasizes the pros and cons of the two fundamentally important paradigms of event-triggered and time-triggered systems. An introduction to the two high-level embedded programming languages Esterel and Giotto will be presented. Esterel is a synchronous reactive language with an event-triggered semantics whereas Giotto has a time-triggered semantics. Giotto has recently been developed at UC Berkeley. Example programs in Esterel and Giotto will be implemented on Lego Mindstorm robots. Each week, a one and a half hour lecture will be presented and a one and a half hour discussion will be held. Goal of the course: Learn how to: evaluate applications with real-time requirements, identify adequate programming paradigm and platform, implement applications with real-time requirements. Literature: - Helmut Kopetz, Real-Time Systems: Design Principles for Distributed Embedded Applications, 1997. - Giorgio C. Buttazzo, Hard Real-Time Computing Systems: Predictable Scheduling Algorithms & Applications, 1997. - Gérard Berry, The Foundations of Esterel, in Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling and M. Tofte, editors, MIT Press, 2000. - Papers on special topics. Controller Design and Analysis ============================== High Confidence Control of Multi-Modal Systems ---------------------------------------------- In multi-modal control paradigm, a set of controllers of satisfactory performance have already been designed and must be used. When such a collection of {\em control modes} is available, an important problem is to be able to accomplish a variety of high level tasks by appropriately switching between the low-level control modes. T. John Koo, George Pappas (University of Pennsylvania), and Shankar Sastry presented a framework for synthesizing a control mode graph which can be used to determine the sequence of control modes that will satisfy reachability tasks. The control mode graph can be used on-line for efficient and dependable real-time mode switching. Our approach is illustrated on a helicopter example, where we determine the mode switching logic that achieves the high-altitude takeoff task from a hover mode. Semi-decidable Synthesis for Triangular Hybrid Systems ------------------------------------------------------ Omid Shakernia, George J. Pappas (University of Pennsylvania), and Shankar Sastry extended recent decidability results on controller synthesis for classes of linear hybrid systems to semi-decision procedures for triangular hybrid systems which could be used to model nonholonomic systems after a transformation. The results were then applied to verification of a conflict resolution maneuver from air traffic control. Global Controllability of Hybrid Systems ---------------------------------------- Ekaterina S. Lemch, Shankar Sastry, Peter E. Caines (McGill University) investigated the question of the global controllability posed for control hybrid systems with autonomous and controlled switchings. The notion of the controlled hybrifold was introduced for analysis. Sufficient conditions for the global controllability are obtained in terms of the so-called hybrid fountains. 2. Interactions and Technology Transfer Interactions ------------ * Weekly SEC meetings, Wednesdays 3-4pm. Topics that were covered include: - Jie Liu about the RTOS domain. - Christoph Kirsch about the software architecture of the ETH helicopter from Zurich, and on the meeting with Loren Shade from Wind River Systems. - Edward Lee about the Ptolemy II release. - John Koo, about Mode Switching Synthesis and architecture for Multi-Modal Control. - Jie Liu about a distributed framework for Ptolemy II. - Tunc Simsek on exception handling for networks of hybrid automata. - Johan Eker about the Integrated Control and RT-system design. - Christoph Kirsch about "The Embedded Machine". * Visit from Zurich -- Marco Sanvido from ETH Zurich visited us. He's the software engineer working on the Zurich helicopter. He gave the following talk at the SEC meeting: "Autonomous Flying Model Helicopter Research at the Federal Institute of Technology, Zurich" Abstract: The presentation will summarize past and future research efforts on autonomous flying model helicopter systems done at the ETHZ Zurich. The systems developed (and in development), the motivation and the technical challenges such as the embedded system design, the control and the flight manager will be presented. * Visit from Konstanz, Germany. Wolfgang Pree, reknown for his textbook on design patterns in embedded software visited us from September 2000 to March 2001. During his stay he integrated Giotto with his software engineering methodology of embedded frameworks. He also taught a course on software engineering, and gave several talks on embedded software design. * We were visited by Stephane Lafortune, Professor of EECS at the University of Michigan, who gave a talk on Decentralized Control of Discrete-Event Systems * January 10 and 11, Brian Mendel and David Corman visited our group for an intensive planning session on the OCP. They raised the "precise mode change problem," which motivated the construction of the RTOS domain. * We conducted a design review of the Java Spaces related classes in Ptolemy II -- TokenEntry, Publisher, Subscriber, and SpaceFinder -- and invited the Boeing visitors to observe and participate in our software development process Jorn will moderate. * Douglas Stuart, from Boeing, worked with David Corman and Brian Mendel (SEC) and David Sharp (MoBIES) at Boeing St. Louis, looking at Ptolemy to see how it could be integrated into the OCP and OEP environments. His task was to build an accutator controler using the Ptolemy II CT (continuous time) domain and have it communicate via the Java ORB with an OCP simulator. Although he found the same ORB incompatibilities that we had found, he stimulated some progress on the CT domain by asking where there was a Ptolemy actor compatible with the CT domain corresponding to the Matlab/Simulink Rate Limiter block, which bounds the derivative of control signals. Jie Liu created such a block for him. * We have begun discussions with Paul Hudak at Yale to get his help on the controls API and to explore the use of FRP in Ptolemy II. On the controls API, we particularly believe he can help with the concept of higher-order components, which are components that take components as parameters and inputs, and can produce components as outputs. Talks ----- * T. Henzinger, "Decomposing Model-checking Tasks using the Assume-guarantee Paradigm," IFIP Working Group 2.3 Meeting, Santa Cruz, California (January 2001). * T. John Koo, "Modeling of Hierarchical Multi-Modal Systems in Ptolemy II," Ptolemy Miniconferenc (Berkeley, CA, 3/22 - 3/23). * Ben Horowitz, "Embedded Control System Development in Giotto," Ptolemy Miniconferenc (Berkeley, CA, 3/22 - 3/23). * Marius Minea, "Assume-guarantee reasoning for hierarchical hybrid systems," Hybrid Systems: Computation and Control (Rome, Italy, 3/28-3/30). * T. J. Koo, G. J. Pappas, and S. Sastry, "Mode Switching Synthesis for Reachability Specifications," Hybrid Systems: Computation and Control (Rome, Italy, 3/28-3/30). Presented by G. J. Pappas. * O. Shakernia, G.J. Pappas, S. Sastry, "Semi-decidable Synthesis for Triangular Hybrid Systems," Hybrid Systems: Computation and Control (Rome, Italy, 3/28-3/30). Presented by O. Shakernia. * E. S. Lemch, S. Sastry, P.E. Caines, "Global Controllability of Hybrid Systems with controlled and Autonomous Switchings," Hybrid Systems: Computation and Control (Rome, Italy, 3/28-3/30). * J. Hu, M. Prandini, K. H. Johansson, S. Sastry, "Hybrid Geodesics as Optimal Solutions to the Collision-Free Motion Planning Problem," Hybrid Systems: Computation and Control (Rome, Italy, 3/28-3/30). Awards ------ Jie Liu won the Leon Chua award at UC Berkeley for contributions to nonlinear science. This award reflects his contributions to continuous-time modeling and hybrid systems. Personnel --------- Johan Eker, from Sweden, has joined as a postdoc. His background is in embedded system/automatic control. He received my PhD in control in December 1999 from Dept. of Automatic Control, Lund Institute of Tech., and stayed an extra year as researcher during 2000. His PhD work focused on integrated design of the control algorithm and the task scheduling mechanism in embedded control systems. The main question he was looking at was 'How will the control performance be affected by specified run-time implementations (e.g. investigate the influence from jitter, delay, etc.)?' He also looked at language support for implementation of flexible embedded control systems, that allowed control algorithms to be edited and replaced on-line. During 2000 he spent most of his time working on distributed wireless control using Bluetooth. Publications ------------ [1] Jie Liu, Xiaojun Liu, and Edward A. Lee, "Modeling Distributed Hybrid Systems in Ptolemy II," invited tutorial to ACC 2001. [2] John Davis II, Christopher Hylands, Bart Kienhuis, Edward A. Lee, Jie Liu, Xia ojun Liu, Lukito Muliadi, Steve Neuendorffer, Jeff Tsay, Brian Vogel, and Yuhong Xiong, "Heterogeneous Concurrent Modeling and Design in Java," Technical Memorandum UCB/ERL M01/12, EECS, University of California, Berkeley, March 15, 2001. [3] Edward A. Lee, "Overview of the Ptolemy Project," Technical Memorandum UCB/ERL M01/11, University of California, Berkeley, March 6, 2001. [4] Jie Liu, Stan Jefferson, and Edward Lee, “Motivating Hierarchical Run-Time Models in Measurement and Control Systems,” invited paper, ACC 2001. [5] T. J. Koo, G. J. Pappas, and S. Sastry, "Mode Switching Synthesis for Reachability Specifications," Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 2034, pp. 331-346, Springer, 2001. [6] O. Shakernia, G.J. Pappas, S. Sastry, "Semi-decidable Synthesis for Triangular Hybrid Systems," Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 2034, pp. 487-500, Springer, 2001. [7] O. Shakernia, G. J. Pappas, S. Sastry, "Semidecidable Controller Synthesis for Classes of Linear Hybrid Systems," IEEE Conf. on Decision and Control, Sydney, AU, December 2000. [8] E. S. Lemch, S. Sastry, P.E. Caines, "Global Controllability of Hybrid Systems with controlled and Autonomous Switchings," Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 2034, pp. 375-386, Springer, 2001. [9] J. Hu, M. Prandini, K. H. Johansson, S. Sastry, "Hybrid Geodesics as Optimal Solutions to the Collision-Free Motion Planning Problem," Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 2034, pp. 305-318, Springer, 2001. [10] T. J. Koo, G. J. Pappas, and S. Sastry, "Multi-Modal Control of Systems with Constraints," submitted to IEEE Conf. on Decision and Control, Orlando, FL, December 2001. [11] T. J. Koo, "Hierarchical System Architecture for Multi-Agent Multi-Modal Systems," submitted to IEEE Conf. on Decision and Control, Orlando, FL, December 2001. [12] Thomas A. Henzinger, Marius Minea, and Vinayak Prabhu. Assume-guarantee reasoning for hierarchical hybrid systems. Proceedings of the Fourth International Workshop on Hybrid Systems: Computation and Control (HSCC 2001), Lecture Notes in Computer Science 2034, Springer-Verlag, 2001, pp. 275-290. 4. Financial Data ----------------- Provided separately on a quarterly basis by the university. APPENDIX A ========== Release Notes for Ptolemy 1.0 ----------------------------- Ptolemy II 1.0 is available for download from http://ptolemy.eecs.berkeley.edu/ptolemyII/ptII1.0 Ptolemy II is a software framework developed as part of the Ptolemy project. It is a Java-based component assembly framework with a graphical user interface called Vergil. Vergil itself is a component assembly defined in Ptolemy II. The Ptolemy project studies modeling, simulation, and design of concurrent, real-time, embedded systems. The focus is on assembly of concurrent components. The key underlying principle in the project is the use of well-defined models of computation that govern the interactions between components. A major problem area being addressed is the use of heterogeneous mixtures of models of computation. The Ptolemy Project web page (http://ptolemy.eecs.berkeley.edu) contains much more information about the project. The work is conducted in the Department of Electrical Engineering and Computer Sciences of the University of California at Berkeley. The project is directed by Prof. Edward A. Lee. The project is named after Claudius Ptolemaeus, the second century Greek astronomer, mathematician, and geographer. Ptolemy II includes a growing suite of domains, each of which realizes a model of computation. It also includes a component library, in which most components are domain polymorphic, in that they can operate in several of the domains. Most are also data polymorphic, in that they operate on several data types. The domains that have been implemented are listed below. Some of these are preliminary and/or experimental, as indicated below. CT: continuous-time modeling DE: discrete-event modeling FSM: finite state machines PN: process networks SDF: synchronous dataflow CSP: communicating sequential processes (experimental) DDE: distributed discrete events (experimental) DT: discrete time (experimental) Giotto: periodic time-driven (experimental) GR: 3-D graphics (experimental) Ptolemy II contains the following features: * Vergil: A block-diagram editor for building models * User interface utilities for applets and applications * Live editing of models and parameters * Network integration * A sophisticated type system including Type constant propagation, Record Types, Array types, and Fixed-point type * An expression language for parameter expressions * Data and domain polymorphic component library * A polymorphic expression actor * A very simple XML file format called MoML * A flexible signal plotter * 3-D graphics animation infrastructure * Hierarchically interoperable domains * On-line documentation (in HTML) * Audio signal processing capabilities The Ptolemy II website contains Ptolemy II applets that can be run by using the Java Plug-in 1.3. Ptolemy II is available for download in two versions: * Ptiny - which can be used to build models in CT, DE, FSM, PN and SDF using built-in actors. The Ptiny version is a 5.6Mb download for Windows. * Full - which includes other domains and support for developing custom actors. The Full version is a 20Mb download for Windows or a 5.3Mb source only download for Windows and Unix.