Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software

  • Xianghua Deng
  • Matthew B. Dwyer
  • John Hatcliff
  • Georg Jung
  • Robby
  • Gurdip Singh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)


Component frameworks such as the CORBA Component Model (CCM) and middleware services such as the CORBA Event Service are increasingly being used to build safety / mission-critical distributed real-time embedded (DRE) systems. In this paper, we present a novel model-checking infrastructure for checking global temporal properties of DRE systems built on top of a Real-Time CORBA Event Service using CCM architectures. We describe how (a) building support for OO structures and communication layers directly in an extensible model-checker and (b) leveraging domain properties related to priorities, scheduling, and timing can dramatically reduce the costs of checking realistic systems.


Model Check Rate Group Event Handler Event Connection Subscriber List 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology (July 1997)Google Scholar
  2. 2.
    Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. International Journal on Software Tools for Technology Transfer. Springer-Verlag (2002)Google Scholar
  3. 3.
    Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder – a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)Google Scholar
  4. 4.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  5. 5.
    Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering (June 2000)Google Scholar
  6. 6.
    de Niz, D., Rajkumar, R.: Geodesic - a reusable component framework for embedded real-time systems. Technical report, Carnegie Mellon University (2002)Google Scholar
  7. 7.
    Demartini, C., Iosif, R., Sisto, R.: dspin: A dynamic extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, p. 261. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Deng, W., Dwyer, M., Hatcliff, J., Jung, G., Robby, Singh, G.: Model-checking middleware-based event-driven real-time embedded software (extended version) (April 2003) (forthcoming)Google Scholar
  9. 9.
    Doerr, B., Sharp, D.: Freeing product line architectures from execution dependencies. In: Proceedings of the Software Technology Conference (May 1999)Google Scholar
  10. 10.
    Eclipse Consortium. Eclipse website (2001),
  11. 11.
    Garlan, D., Khersonsky, S.: Model checking implicit-invocation systems. In: Proceedings of the 10th International Workshop on Software Specification and Design (November 2000)Google Scholar
  12. 12.
    Goessler, G., Sifakis, J.: Composition for component-based modeling. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 443–466. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Harrison, T.H., Levine, D.L., Schmidt, D.C.: The design and performance of a real-time corba event service. In: Proceedings of the 1997 ACM SIGPLAN conference on Object-oriented programming systems, languages and applications, pp. 184–200. ACM Press, New York (1997)CrossRefGoogle Scholar
  14. 14.
    Hatcliff, J., Deng, W., Dwyer, M., Jung, G., Prasad, V.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proceedings of the 25th International Conference on Software Engineering (2003) (to appear)Google Scholar
  15. 15.
    Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (1999)Google Scholar
  16. 16.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)CrossRefMathSciNetGoogle Scholar
  17. 17.
    Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proceedings of Third International SPIN Workshop (April 1997)Google Scholar
  18. 18.
    Iosif, R.: Symmetry reduction criteria for software model checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 22–41. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  19. 19.
    Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing 11(6), 637–664 (1999)zbMATHCrossRefGoogle Scholar
  20. 20.
    Lee, E.A.: Overview of the ptolemy project. Technical Report UCB/ERL M01/11, University of California, Berkeley (March 2001)Google Scholar
  21. 21.
    Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering (1999)Google Scholar
  22. 22.
    Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 2003 ACM Symposium on Foundations of Software Engineering, FSE 2003 (2003)Google Scholar
  23. 23.
    Robby, Dwyer, M.B., Hatcliff, J.: Bogor Website (2003),
  24. 24.
    Sipma, H.: Event correlation: A formal approach. Technical Report Draft, Stanford University (July 2002)Google Scholar
  25. 25.
    Vestal, S.: Metah user’s manual (1998),

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Xianghua Deng
    • 1
  • Matthew B. Dwyer
    • 1
  • John Hatcliff
    • 1
  • Georg Jung
    • 1
  • Robby
    • 1
  • Gurdip Singh
    • 1
  1. 1.Department of Computing and Information SciencesKansas State UniversityManhattanUSA

Personalised recommendations