Specification and Automated Analysis

To help design and prototype resource-sensitive, real-time systems, we have developed a specification model called Communicating Shared Resources (CSR). Processes are specified in a high-level, concrete syntax, which includes constructs for priority, deadlines, periodicity and exception-handling [Info&Comp94]. The theory underlying CSR has led to the development of an automated toolset that developers can easily use. One such tool is a reachability analyzer [TSE92], in which a specification is compiled into state-transition system, and the states are checked for real-time exceptions. Another is a theorem proof-assistant, which mechanically helps a designer check proofs for real-time safety. We have extended this work to Ada multi-tasking programs [Compass94, ISSTA96], which has resulted in an analysis engine to check for subtle safety and liveness errors. The tool works by (1) compiling individual tasks into simple state-transition models, and (2) compositionally checking the entire program for conformance to its specification. This checking is done in an iterative, piece-by-piece manner, in that local analysis is first performed on the individual tasks, and as tasks are composed, more analysis is carried out. The objective here is to progressively delete states that are known to disprove the specification, so that the generated state-space is kept to a minimum. This result of the algorithm is a composite state space which is significantly smaller than that of the original program.

The analysis engine is fairly mature at this point: it comprises roughly 70,000 lines of C++ and C code, as well as standard C++ templates, yacc generation code, etc.

We are currently investigating model-checking on infinite-state programs [ CAV97]. In infinite transition systems, the problem gets substantially harder -- and many basic properties are undecidable. Hence we are attacking the problem using conservative techniques, in concert with a symbolic model checker, which uses Presburger formulas to encode a program's transition system (as well as its model-checking computations). Fixpoint calculations are executed symbolically, and their convergence is guaranteed by using several approximation techniques. This method has yielded some very promising results; to date, it was successfully verified safety and liveness properties on several infinite-state systems, commonly used in standard concurrency applications.

However, we also discovered that our pure Presburger approach was inefficient in its treatment of Boolean and (unordered) enumerated types -- which possess no natural mapping to the Euclidean coordinate space.

To correct this problem, we developed a new set of verification techniques, which combine the strengths of both approaches. Specifically, this resulted in a composite model-checker, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. To date, we have demonstrated our technique's effectiveness on some nontrivial requirements specifications, which include mixtures Booleans, integers and enumerated types [Composite97].