Skip to main content
SpringerLink
Log in

Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System

  • Conference paper
Component-Based Software Engineering (CBSE 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4063))

Included in the following conference series:

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 Number CCF-0438971 and CCF-0609612.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 9th Annual Symposium on Foundations of Software Engineering (FSE), pp. 109–120. ACM Press, New York (2001)

    Google Scholar 

  3. Attie, P.C., Chockler, H.: Automatic verification of fault-tolerant register emulations. In: Proceedings of the Infinity 2005 workshop (2005)

    Google Scholar 

  4. Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM Transactions on Programming Languages and Systems 20(1), 51–115 (1998)

    Article  Google Scholar 

  5. Attie, P.C.: Synthesis of large concurrent programs via pairwise composition. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Attie, P.C.: Synthesis of large dynamic concurrent programs from dynamic specifications. Technical report, American University of Beirut (2005), available at: http://www.cs.aub.edu.lb/pa07/files/pubs.html

  7. Attie, P.C., Lorenz, D.H.: Correctness of model-based component composition without state explosion. In: ECOOP 2003 Workshop on Correctness of Model-based Software Composition (2003)

    Google Scholar 

  8. Cheung, S., Giannakopoulou, D., Kramer, J.: Verification of liveness properties in compositional reachability analysis. In: Jazayeri, M. (ed.) ESEC 1997 and ESEC-FSE 1997. LNCS, vol. 1301. Springer, Heidelberg (1997)

    Google Scholar 

  9. Cheung, S., Kramer, J.: Checking subsystem safety properties in compositional reachability analysis. In: Proceedings of the 18th International Conference on Software Engineering, ICSE 1996, Berlin, Germany. IEEE Computer Society Press, Los Alamitos (1996)

    Google Scholar 

  10. Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(2) (1996)

    Google Scholar 

  11. Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450–462. Springer, Heidelberg (1993)

    Google Scholar 

  12. Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  13. Clarke, E.M., Long, D., McMillan, K.L.: Compositional model checking. In: Proceedings of the 4th IEEE Symposium on Logic in Computer Science. IEEE, New York (1989)

    Google Scholar 

  14. Crnkovic, I., Schmidt, H., Stafford, J., Wallnau, K. (eds.): Proceedings of the 4th ICSE Workshop on Component-Based Software Engineering: Component Certification and System Prediction, Toronto, Canada. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  15. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–477. Springer, Heidelberg (1993)

    Google Scholar 

  16. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design: An International Journal 9(1/2), 105–131 (1996)

    Article  Google Scholar 

  17. Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J.V. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B. MIT Press/Elsevier, Cambridge (1990)

    Google Scholar 

  18. Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)

    Article  Google Scholar 

  19. Heineman, G.T., Councill, W.T. (eds.): Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley, Reading (2001)

    Google Scholar 

  20. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)

    Google Scholar 

  21. Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, San Francisco (2003)

    Google Scholar 

  22. Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, Toronto, Canada. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  23. Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1), 203–243 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  24. Kesten, Y., Pnueli, A., Vardi, M.Y.: Verification by augmented abstraction: The automata-theoretic view. Journal of Computer and System Sciences 62(4), 668–690 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  25. Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 402–423. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  26. Lorenz, D.H., Petkovic, P.: ContextBox: A visual builder for context beans (extended abstract). In: Proceedings of the 15th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 2000, pp. 75–76. ACM SIGPLAN, Minnesota (2000)

    Chapter  Google Scholar 

  27. Lorenz, D.H., Petkovic, P.: Design-time assembly of runtime containment components. In: Li, Q., Firesmith, D., Riehle, R., Pour, G., Meyer, B. (eds.) Proceedings of the 34th International Conference on Technology of Object-Oriented Languages and Systems, Santa Barbara, CA, pp. 195–204. IEEE Computer Society, Los Alamitos (2000)

    Chapter  Google Scholar 

  28. Lorenz, D.H., Vlissides, J.: Designing components versus objects: A transformational approach. In: [22], pp. 253–262 (2001)

    Google Scholar 

  29. Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, 219–246 (1989)

    Google Scholar 

  30. Lynch, N., Vaandrager, F.: Forward and backward simulations — part I: Untimed systems. Information and Computation 121(2), 214–233 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  31. Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)

    MATH  Google Scholar 

  32. Mäkinen, E., Systä, T.: MAS - an interactive synthesizer to support behavioral modeling in UML. In: [22], pp. 15–24 (2001)

    Google Scholar 

  33. Pnueli, A.: The temporal logic of programs. In: IEEE Symposium on Foundations of Computer Science, pp. 46–57. IEEE Press, Los Alamitos (1977)

    Google Scholar 

  34. Szyperski, C.: Component Software, Beyond Object-Oriented Programming. Addison-Wesley, Reading (1997)

    Google Scholar 

  35. Vanderperren, W., Wydaeghe, B.: Towards a new component composition process. In: Proceedings of the 8th International Conference on the Engineering of Computer Based Systems, ECBS 2001, pp. 322–331. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  36. Vanderperren, W., Wydaeghe, B.: Separating concerns in a high-level component-based context. In: Easy Comp. Workshop at ETAPS 2002 (2002)

    Google Scholar 

  37. Vanderperren, W.: A pattern based approach to separate tangled concerns in component based development. In: Proceedings of the 1st AOSD Workshop on Aspects, Components, and Patterns for Infrastructure Software, ACP4IS 2002, Enschede, The Netherlands, pp. 71–75 (2002)

    Google Scholar 

  38. Wallnau, K.C., Hissam, S., Seacord, R.: Building Systems from Commercial Components. In: Software Engineering. Addison-Wesley, Reading (2001)

    Google Scholar 

  39. Wydaeghe, B., Vanderperren, W.: Visual component composition using composition patterns. In: Proceedings of the 39th International Conference on Technology of Object-Oriented Languages and Systems, Santa Barbara, CA, pp. 120–129. IEEE Computer Society, Los Alamitos (2001)

    Chapter  Google Scholar 

  40. Wydaeghe, B.: PACOSUITE: Component composition based on composition patterns and usage scenarios. PhD thesis (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. American University of Beirut, Beirut, Lebanon

    Paul C. Attie

  2. University of Virginia, Charlottesville, VA, 22904, USA

    David H. Lorenz

  3. Northeastern University, Boston, MA, 02115, USA

    Aleksandra Portnova

  4. WPI, Worcester, MA, 01609, USA

    Hana Chockler

Authors
  1. Paul C. Attie
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David H. Lorenz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Aleksandra Portnova
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Hana Chockler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Pacific Northwest National Laboratory, Computational and Information Sciences, MS: K7-90,, PO Box 999,, 99352, Richland, WA, USA

    Ian Gorton

  2. Department of Computer Science, Worcester Polytechnic Institute, 100 Institute Road, 01609, Worcester, MA, USA

    George T. Heineman

  3. School of Innovation, Design and Engineering, Mälardalen University, Västerås, Sweden

    Ivica Crnković

  4. Centre for Distributed Systems and Software Engineering, Monash University, Melbourne, Australia

    Heinz W. Schmidt

  5. Computer Science, Tufts University, Boston, 161 College Avenue, 02155, Medford, MA, USA

    Judith A. Stafford

  6. Microsoft, USA

    Clemens Szyperski

  7. Software Engineering Institute,  

    Kurt Wallnau

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Attie, P.C., Lorenz, D.H., Portnova, A., Chockler, H. (2006). Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System. In: Gorton, I., et al. Component-Based Software Engineering. CBSE 2006. Lecture Notes in Computer Science, vol 4063. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11783565_3

Download citation

  • DOI: https://doi.org/10.1007/11783565_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35628-8

  • Online ISBN: 978-3-540-35629-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation