Validation of Object-Oriented Concurrent Designs by Model Checking

  • Klaus Schneider
  • Michaela Huhn
  • George Logothetis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


Reusability and evolutivity are important advantages to introduce objectoriented modeling and design also for embedded systems [1 2]. For this domain, one of the most important issues is to validate the interactions of a set of object with concurrent methods. We apply model checking (see [3] for a survey) for the systematic debugging of concurrent designs to detect errors in the behavior and interactions of the object community. As we assume a fixed finite maximal number of objects and also finite data types, we can only show the correctness for finite instances and detect only errors that appear in such a finite setting. Nevertheless, the approach is useful for embedded systems, where the system’s size is limited by strong hardware constraints. Moreover, we claim that most errors in the concurrent behavior already occur with a small number of components. To handle larger designs, we emphasize that it is often obvious that several attributes of an object do not affect the property of interest. Thus, there is no need to model the objects completely. This obvious abstraction leads to significantly better results because the resulting models are smaller. More sophisticated abstractions can be found e.g. in [4 5]. In the next section, we briefly explain how to derive in general a finite state system from an object-oriented concurrent design. Then, we illustrate the method by a case study taken from [6].


  1. 1.
    W. Nebel and G. Schumacher. Object-oriented hardware modelling: Where to apply and what are the objects. In Euro-Dac’ 96 with Euro-VHDL’ 96, 1996.Google Scholar
  2. 2.
    J. S. Young, J. MacDonald, M. Shilman, P. H. Tabbara, and A. R. Newton. Design and specification of embedded systems in Java using successive, formal refinement. In Design Automation Conference (DAC’98), 1998.Google Scholar
  3. 3.
    E. M. Clarke, O. Grumberg, and D. E. Long. Model checking. volume 152 of Nato ASI Series F. Springer-Verlag, 1996.Google Scholar
  4. 4.
    E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and systems, 16(5):1512–1542, September 1994.CrossRefGoogle Scholar
  5. 5.
    C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1–35, February 1995.CrossRefGoogle Scholar
  6. 6.
    F. Schön and W. Schröder-Preikschat. On the interrupt-transparent synchronization of interrupt-driven code. Arbeitspapiere der GMD, GMD Forschungszentrum Informatik, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Klaus Schneider
    • 1
  • Michaela Huhn
    • 1
  • George Logothetis
    • 1
  1. 1.Institute for Computer Design and Fault ToleranceUniversity of Karlsruhe Department of Computer ScienceKarlsruheGermany

Personalised recommendations