We focus on component based software verification and early (design time) error detection based on a behavioral type system defining temporal properties of software component interfaces.
Interface theories are a very general formalism for expressing design time assumptions made by a component about the behavior of the environment it is to be deployed in, and have been used in a wide variety of systems, concurrent, single-threaded, asynchronous, synchronous, recursive, etc. [1-5], and used to express many kinds of environment assumptions.
We focus on interfaces for software systems involving recursive programs and expressing method invocation protocols . Checking compatibility of two systems in this context involves solving a reachability game with two players on the configuration graph of a pushdown automaton.
There are several interesting applications of this treatment. It is possible to detect incompatiblities between components locally. For example, we have found method call order protocol violation errors in the TinyOS system, an operating system for ad-hoc networked sensors developed by systems researchers at UC Berkeley.
We have implemented CHIC, a checker for checking compatibility of a variety of interface formalisms. CHIC is available as a plug-in for the popular Java IDE, JBuilder.
The standard refinement approach for verifying systems consists of constructing an abstract model of the system, proving properties on the abstract level, and finally showing that the real model is a refinement of the abstract model, i.e., every trace in the actual model is present in the abstract one. In many control systems applications, the ultimate objective is to show that the system stays within some parameters. A slight deviation from the ideal behavior may be acceptable provided some constraints are not violated. We are working on a notion of refinement which considers metrics between traces. The standard refinement relation looks at the Boolean metric on traces--either the two traces are the same, or they are not. Approximate refinement uses metrics for which the distance between traces can have a gradient. It quantifies the degree to which the actual system model is close to the abstract one. The designers can decide what degree of closeness they desire. Exact trace inclusion may not be required as the model of the system may be only an approximation of the real world dynamics.
1Former Postdoctoral Researcher
Giotto is a real-time programming language for control systems. A control application typically consists of communicating periodic tasks, together with mode switches that enable and disable tasks. We are pursuing two lines of research relating to Giotto:
(1) Scheduling theory for Giotto. Giotto is platform-independent, and thus does not specify in detail how Giotto programs are to be scheduled. The Giotto compiler's current scheduling algorithm interprets Giotto's operational semantics quite literally. We are investigating how this literal interpretation may be relaxed, allowing more Giotto programs to be scheduled. Our starting point is precedence-constrained scheduling models, drawn from the scheduling theory literature. Single-mode, single-processor Giotto programs may be modeled as periodic instances of 1 | rj; dj; prec; pmtn | - (the problem of scheduling dependent tasks with release times, deadlines, and preemption on a single processor). Using a novel extension of standard earliest deadline first scheduling algorithms, I have developed an algorithm for schedule synthesis that captures interesting schedule optimizations and is polynomial-time. One direction in which these results can be generalized is multi-mode programs. I have developed a novel model, of conditional scheduling problems, that captures the branching behavior of multi-mode programs, and permits the synthesis of schedules in polynomial time. Another direction in which these results might be generalized is multi-processor programs. For distributed and multi-CPU settings, almost all precedence-constrained scheduling models are NP-hard, so I am focusing instead on load-balancing approximation algorithms. This work is being done in conjunction with Tom Henzinger.
(2) A Giotto-based helicopter control system. In conjunction with this theoretical work, we are implementing a Giotto-based helicopter control system for a Yamaha RMAX helicopter, with two goals in mind. The first goal is to produce a modular implementation. The control computer must be prepared to communicate with a wide variety of sensors--global positioning system, inertial measurement unit, etc.--each with its own data format and timing behavior. To manage the complexity in the helicopter control system, we use platform-based design, which introduces multiple layers of abstraction between application and implementation. The second goal is to produce a testable implementation. Since testing the control system on the actual helicopter is time consuming and somewhat risky, we have built a hardware-in-the-loop simulator for the Yamaha RMAX. The idea is to replace the helicopter itself with a simulated model of the helicopter's dynamics. The control system, however, remains the same, and may be tested against the simulator rather than the helicopter itself. This work is being done in conjunction with Judy Liebman, Cedric Ma (who have both graduated), John Koo, Tom Henzinger, Alberto Sangiovanni-Vincentelli, and Shankar Sastry.
Figure 1: Precedence constraints for a single-mode Giotto program
We consider programs of the so-called embedded (E) machine, which is a virtual machine for coordinating the interaction between physical processes and software processes . The E machine executes E code, the timing and control-flow part of a program that specifies the invocation of software processes relative to events. The software processes form the functional part of the program and among them we distinguish two kinds: drivers and tasks. All information between the environment and the tasks flows through drivers, software processes with negligible worst-case execution times (WCET). On the other hand, tasks model processes with nonnegligible WCETs. One way to generate E code is from Giotto, a language designed for multi-modal control applications, where each mode is specified with a set of tasks and drivers that are periodically invoked.
The project addresses the problem of checking whether all possible executions of a given E code program on a given platform satisfy certain timing requirements. The compiler that generates E code expects sufficient performance from the platform, so that the computation of a task always finishes before drivers update task inputs or read task outputs, and before another invocation of the task is scheduled. A trace that satisfies such implicit deadlines is called time safe because it meets all timing requirements of the E code.
In  we show that time-safety checking of arbitrary E code is computationally hard. However, a large class of real-time programs can be expressed as restricted subclasses of general E code. For example, a Giotto source program compiled into E code in a specific way can be checked in polynomial time. In this project we will try to exploit the E code structure further to construct efficient algorithms for time-safety checking. We envision an algorithm with two parts. It first computes the deadlines and then checks if the set of tasks with given WCETs and computed deadlines can be scheduled by a specified scheduling strategy. The algorithm does not interpret conditionals in the E code: the deadline is conservatively approximated as the minimum of the deadlines from the two branches of a conditional. The check is performed by building a program graph on E code extended with particular scheduler states.
The BLAST tool implements a counterexample guided abstract model checking algorithm for model checking safety properties of C programs. A predicate abstraction of the C program is constructed on the fly along with the model checking, and the abstraction is refined locally using infeasible counterexample traces. The tool takes as input a C program and a safety monitor written in C syntax, and checks if the program satisfies the safety property specified by the monitor. If the property fails to hold, BLAST produces a counterexample trace in the source program witnessing the failure. If the property holds, the tool presents an easily checkable proof of correctness using program invariants found in the model checking. The process is automatic, in particular, no programmer annotations are required. We have used BLAST to model check safety properties of several Windows and Linux device drivers. We have found several bugs in the drivers, and provided short proofs for correct drivers.
We have extended the algorithm of BLAST in two directions: to check more expressive properties, and to work on concurrent programs. We have extended counterexample guided model checking to check controllability of linear time temporal logic properties. As a special case, this gives a counterexample guided model checking algorithm for linear time temporal logic verification (of which safety checking is a special case). We have also extended the implementation to check for race conditions in multi-threaded C programs using thread modular reasoning.
Composing intellectual property blocks is an essential element of a design methodology based on re-use. The composition of these blocks when the IPs have been developed by different groups inside the same company, or by different companies, is notoriously difficult. Design rules in the form of interface specifications have been proposed which try to alleviate the problem by forcing the designers to be precise about the behavior of the individual components, and to verify this behavior under a number of assumptions about the environment in which they have to operate. In this work we study the problem of the specification, synthesis, and verification of interfaces for different models of computation and across models of computation. This work supports the Metropolis Meta-Model in the construction of a system integration platform that can integrate heterogeneous models.
Roughly speaking, two agents are compatible if they fit together as they are. In this work we formalize this notion by introducing, for each model of computation, a set of agents that “behave well,” and by deriving a refinement ordering that represents substitutability, called the conformance ordering. We show that under certain assumptions we can represent the set of compatible agents by a single maximal environment, called a mirror. Two agents are compatible if one conforms to the maximal environment of the other.
When components are taken from legacy systems or from third-party vendors, it is likely that their interface communication protocols are not compatible. In this case, an additional adapter can sometimes be introduced to convert from one agent to the other so that their composition is compatible. The notion of a maximal environment allows us to formulate a synthesis algorithm for an adapter that conforms to the specification of a desired communication.
We formulate the problem in particular for synchronous and asynchronous systems. We use an automata-based and a game-theoretic based approach to solving the adaptation problem and to synthesize a converter between two specified protocols.