Behavioral Compatibility without State Explosion: Design and Verification of a Component-based Elevator Control System

Paul C. Attie, American University of Beirut
David H. Lorenz, University of Virginia
Aleksandra Portnova, Northeastern University
Hana Chockler, WPI

Abstract: Most methods for designing component-based systems and verifying their compatibility address only the syntactic compatibility of components; no analysis of run-time behavior is made. Those methods that do address run-time behavior suffer from state-explosion: the exponential increase of the number of global states, and hence the complexity of the analysis, with the number of components. We present a method for designing component-based systems and verifying their behavioral compatibility and temporal behavior that is not susceptible to state explosion. Our method is mostly automatic, with little manual deduction required, and does not analyze a large system of connected components at once, but instead analyzes components two-at-a-time. This pair-wise approach enables the automatic verification of temporal behavior, using model-checking, in time polynomial in the number and size of all components. Our method checks that behavior of a pair of interacting components conforms to given properties, specified in temporal logic. Interaction of the components is captured in a product of their behavioral automata, which are provided as a part of each component's interface. We demonstrate the effectiveness of our method by applying it to the design and verification of a component-based elevator control algorithm. This work was supported in part by NSF’s Science of Design program under grants numbered CCF-0438971 and CCF-0609612, and by the Program for Secure and Dependable Computing at University of Virginia.

In Proceedings of the 9th International Symposium on Component-Based Software Engineering, LNCS 4063, pp. 33-49, 2006.

---

http://dx.doi.org/10.1007/11783565_3

fulltext.pdf

---

@String{LNCS = "Lecture Notes in Computer Science"}
@String{sv = "Springer Verlag"}
@InProceedings{Attie:2006:BCS,
 Author = "Paul Attie and David H. Lorenz and Aleksandra Portnova and Hana Chockler",
 Title = "Behavioral Compatibility without State Explosion:
         {Design} and Verification of a Component-based Elevator Control System",
 Year = 2006,
 BookTitle = "Proceedings of the 9th International Symposium on Component-Based Software Engineering",
 Number =  4063,
 Series = LNCS,
 Pages = "33--46",
 Publisher = sv,
 Editor = "I. Gorton et al.",
}

Related papers:

@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",
  Note         = "\url{http://www.cs.virginia.edu/~lorenz/papers/cmc03/}",
}

@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}",
}