Establishing Behavioral Compatibility of Software Components without State Explosion
Paul Attie, Northeastern UniversityDavid H. Lorenz, Northeastern University
We present a methodology for designing component-based systems and verifying the temporal behavior properties of such systems. Our verification method is mostly automatic, with very little manual deduction re quired. Our verification method is not susceptible to the well-known \emph{state explosion} problem, which has hitherto severely limited thepractical applicability of automatic verification methods. Our method specifies the externally visible behavior of each component $C$ as several interface automaton, one for each of the other components which $C$ interacts directly with. For each pair of directly interacting components, we compute the product of the interface automata. These ``pair machines'' can then be verified mechanically, since they are small. The verified ``pair properties'' can then be combined to deduce global properties. This combination is done deductively, and is quite simple, since the hard work of verifying the pair-properties has already been done. Our case study of an elevator example will substantiate this point. Another contributuion of this paper is the use of several interface automata per component. This enables a clean separation between interfaces, so that the interactions of a component $C$ with several others are cleanly separated, and can be inspected in isolation. Our method also enhances extensibility. If a component is modified, only the pairs in which that component is involved are affected. The rest of the system is undisturbed. We illustrate our method by designing and verifying an elevator example, a standard example in the software engineering literature. To our knowledge, our method is the first approach to behavioral compatibility that does not suffer from state-explosion.
Technical Report NU-CCIS-03-02,
College of Computer and Information Science, Northeastern University, March 2003.
This research was partially supported by
the National Science Foundation under
award number CCR-0204432.
NU-CCIS-03-02.ps.gz (17 pages)
NU-CCIS-03-02.pdf (17 pages)
@TechReport{Attie:2003:EBC,
Title = "Establishing Behavioral Compatibility of Software Components without State Explosion",
Author = "Paul~C. Attie and David~H. Lorenz",
Number = "{NU-CCIS-03-02}",
Institution = "College of Computer and Information Science, Northeastern University",
Address = "Boston, MA 02115",
Month = mar,
Year = 2003,
URL = "http://www.ccs.neu.edu/home/lorenz/papers/reports/NU-CCIS-03-02.html",
}