SEC Meeting: Project Outlines -- part II

Feb. 14, 2000.
4pm - 5pm
Hughes Room

Moderator: Edward A. Lee

Project outlines

• Rich APIs for Real-Time and Embedded-System Design

  Luca de Alfaro,  Tom Henzinger,  Benjamin Horowitz,  and Christoph Meyer

  In component-based design, systems are created by combining preexisting components with new software that provides both glue between the components, and new functionality. This building-block approach to system design requires methods for matching component interfaces and building glue between components. In order to plug an off-the-shelf component into a new design, the full benefits of the component can be derived only if the component comes with a precise specification of, first, how the outputs behave, and second - and equally important - how the component expects the inputs to behave. Currently, such interface specifications are usually based on an informal, English-based description of the functionality, the only formal information being input and output type information for function calls.

  We propose to develop a theory for the composition and analysis of rich application program interfaces (R-API) for embedded programs, which expose resource properties, such as real-time assumptions and guarantees, in addition to type information. The R-API specifications will be able to capture real-time guarantees, as well as probabilistic properties connected to performance and reliability, such as the probability of a message being delivered within a specified time bound. These specifications will relate the behavior of the various API components; as a simple example, it will be possible to formalize statements such as: "the time required for service A is at most twice the context-switch time, plus 1000 processor cycles, plus the time of servicing request B". In developing the specification language, we will aim at simplicity and automated analysis, rather than expressive power. We plan apply R-APIs to the design, validation, and porting of real-time applications:

  • To support the design process, we plan to develop techniques for the compile-time checking of R-APIs specifications against overall system requirements. These techniques will be based on assume-guarantee reasoning about the R-API capabilities and the system requirements.
  • For the validation of real-time systems, R-APIs lead to an approach in which the validation task is decomposed in two largely independent phases: the validation that each component satisfies its specification, and the validation that the overall system goals are met, given the component specifications. For the latter phase, we can use the component specifications to construct a simulation environment that exibiths worst-case component behavior, and validate the system with respect to such an environment.
  • The ability to validate a system with respect to worst-case component behavior also helps in porting the design to different architectures. In fact, in porting the design we can check at compile time that the system requirements are met by the R-APIs guarantees available in the new architecture.
• Framework (Kees)
• UAV Control Software in Software Enabled Control (David)
  UC Berkeley UAV reserach team, BEAR, have been developing a somplete testbed of multiple UAVs and UGVs, communicating via peer-to-peer wireless network system. While UGV and other supporting computation and communication components are mature technologies and available as off-the-shelf products,  UAV technology is relatively new and a lot of research efforts should be made on helicopter model identification, linear/nonlinear control, flight management and so on.

  Each UAV consists of navigation sensors, onboard computer(s), communication systems and actuators. The vehicle management system (VMS) software for RUAV has been written in C running on real-time operating system, QNX. The software takes the responsibility to maintain navigation sensors incluing INS/GPS, download its flight status and process the uploaded request, and issues the control output calculated using control law. Since the software has jobs running at different but constant rates, the software is divided into three different concurrent processes and communicate with one another via interprocess communication protocols supported by QNX.

  Up to now, a onboard flight control algorithm for attitude, velocity, position and heading control has been implemented based on a identified system linear model. This lowest-level regulation layer will be integrated with higher level trajectory generator and flight management layers. Due to the high complexity of the hierarchical control algorithm and many independent and "smart" components such as INS and GPS, operated by independent DSP chips, the onboard software calls for careful job description. This effort has been made in collaboration with Professor Edward Lee, John Koo, and Xiaojun Liu. Also, to manage the resources of the onboard computer and connected components more efficiently and in a more systematic way, the possibility to introduce a resource broker, such as CORBA, are also being reviewed.