Correctness of Model-based Component Composition without State Explosion

Paul C. Attie, Northeastern University
David H. Lorenz, Northeastern University

We present a methodology for designing component-based systems and verifying their temporal behavior properties. Our verification method is mostly automatic, and is not susceptible to the well-known state-explosion problem, which has hitherto severely limited the practical applicability of automatic verification methods. Our method specifies the externally visible behavior of each component $C$ as several behavioral interface automaton (BIA), one for each of the other components which $C$ interacts directly with. A BIA is a finite-state automaton whose transitions can be labeled with method calls. For each pair of directly interacting components, we compute the product of the BIA. These ``pair machines'' are then verified mechanically. The verified ``pair properties'' are then combined deductively to deduce global properties. Since the pair-machines are the product of only two components, they are small, and so their mechanical verification, e.g., by model checking, does not run up against state-explosion. The use of several BIA per component enables a clean separation between interfaces, so that the interactions of a component $C$ with several other components are cleanly separated, and can be inspected in isolation. This in itself promotes the understandability of a design. 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. To our knowledge, our method is the first approach to behavioral compatibility that does not suffer from state-explosion.

In Proceedings of the ECOOP 2003 Workshop on Correctness of Model-based Software Composition. Darmstadt, Germany, July 22, 2003.


main.html (html)

main.ps.gz (28k)

main.pdf (108k)


@InProceedings{Attie:2003:CMC,
 Author = "Paul Attie and David H. Lorenz",
 Title = "Correctness of Model-based Component Composition without State Explosion",
 Year = 2003,
 BookTitle = "ECOOP 2003 Workshop on Correctness of Model-based Software Composition",
 Editors = "Ragnhild Van Der Straeten and Andreas Speck and Elke Pulvermueller and Matthias Clauss and Andreas Pleuss",
}
Related reports:
@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,
  Note         = "\url{http://www.ccs.neu.edu/home/lorenz/papers/reports/NU-CCIS-03-02.html}",
}
@TechReport{Aytar:2003:IES,
  Title       = "An Implementation of an Elevator System in the IOA Language and Toolset",
  Author      = "Onur Aytar and Paul~C. Attie and David~H. Lorenz",
  Number      = "{NU-CCIS-03-04}",
  Institution = "College of Computer and Information Science, Northeastern University",
  Address     = "Boston, MA 02115",
  Month       = mar,
  Year        = 2003,
  Note         = "\url{http://www.ccs.neu.edu/home/lorenz/papers/reports/NU-CCIS-03-04.html}",
}