Compositional Checking of Communication among Observers

  • Ralf Pinger
  • Hans-Dieter Ehrich
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2029)


Observers are objects inside or outside a concurrent object system carrying checking conditions about objects in the system (possibly including itself). In a companion paper [EP00], we show how to split and localise checking conditions over the objects involved so that the local conditions can be checked separately, for instance using model checking. As a byproduct of this translation, the necessary communication requirements are generated, taking the form of RPC-like action calls (like in a CORBA environment) among newly introduced communication symbols. In this paper, we give an algorithmic method that matches these communication requirements with the communication pattern created during system specification and development. As a result, correctness of the latter can be proved. In case of failure, the algorithm gives warnings helping to correct the communication specification.


compositionality distributed logic model checking modelling and design object system temporal logic verification 


  1. [AL93]
    Martin Abadi and Leslie Lamport. Composing Specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, January 1993.CrossRefGoogle Scholar
  2. [AL95]
    Martin Abadi and Leslie Lamport. Conjoining Specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, 1995.CrossRefGoogle Scholar
  3. [CE81]
    Edmund M. Clarke and E. Allen Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. Lecture Notes in Computer Science, 131:52–71, 1981.Google Scholar
  4. [CGP00]
    Edmund M. Clarke, Orna Grumberg, and Doran A. Peled. Model Checking. MIT Press, 2000.Google Scholar
  5. [CLM89]
    E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional Model Checking. In Proceedings fo the 4th Annual Symposium on Principles of Programming Languages, pages 343–362, 1989.Google Scholar
  6. [DH97]
    G. Denker and P. Hartel. Troll-An Object Oriented Formal Method for Distributed Information System Design: Syntax and Pragmatics. Informatik-Bericht 97-03, Technische Universitat Braunschweig, 1997.Google Scholar
  7. [dNV90]
    Rocco de Nicola and Frits Vaandrager. Action versus State based Logics for Transition Systems. In I. Guessarian, editor, Semantics of Concurrency, volume 469 of Lecture Notes in Computer Science, pages 407–419, 1990.Google Scholar
  8. [dR97]
    Willem-Paul de Roever. The Need for Compositional Proof Systems: A Survey. In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science, pages 1–22, September 1997.Google Scholar
  9. [EC00]
    H.-D. Ehrich and C. Caleiro. Specifying communication in distributed information systems. Acta Informatica, 36 (Fasc. 8):591–616, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  10. [ECSD98]
    H.-D. Ehrich, C. Caleiro, A. Sernadas, and G. Denker. Logics for Specifying Concurrent Information Systems. In J. Chomicki and G. Saake, editors, Logics for Databases and Information Systems, pages 167–198. Kluwer Academic Publishers, 1998.Google Scholar
  11. [EP00]
    H.-D. Ehrich and R. Pinger. Checking object systems via multiple observers. In International ICSC Congress on Intelligent Systems & Applications (ISA’2000), volume 1, pages 242–248. University of Wollongong, Australia, International Computer Science Convetions (ICSC), Canada, 2000.Google Scholar
  12. [FM95]
    Jose Luiz Fiadeiro and Tom Maibaum. Verifying for Reuse: Foundations of Object-Oriented System Verification. In C. Hankin, I. Makie, and R. Nagarajan, editors, Theory and Formal Methods, pages 235–257. World Scientific Publishing Company, 1995.Google Scholar
  13. [GKK+98]
    A. Grau, J. Küster Filipe, M. Kowsari, S. Eckstein, R. Pinger, and H.-D. Ehrich. The Troll Approach to Conceptual Modelling: Syntax, Semantics and Tools. In T.W. Ling, S. Ram, and M.L. Lee, editors, Proc. of the 17th Int. Conference on Conceptual Modeling (ER’98), Singapore, pages 277–290. Springer, LNCS 1507, November 1998.Google Scholar
  14. [GL94]
    Orna Grumberg and David E. Long. Model Checking an Modular Verfication. ACM Transactions on Programming Languages and Systems, 16(3):843–871, 1994.CrossRefGoogle Scholar
  15. [HDK+97]
    P. Hartel, G. Denker, M. Kowsari, M. Krone, and H.-D. Ehrich. Information systems modelling with Troll formal methods at work. In Information Systems, volume 22, pages 79–99, 1997.CrossRefGoogle Scholar
  16. [HR00]
    Michael R. A. Huth and Mark D. Ryan. Logic in Computer Science-Modelling and reasoning about systems. Cambridge University Press, 2000.Google Scholar
  17. [Jos89]
    Bernhard Josko. Verifying the Correctness of AADL Modules using Model Checking. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 386–400, 1989.Google Scholar
  18. [MC81]
    Jayadev Misra and K. Mani Chandy. Proofs of Networks of Processes. IEEE Transactions on Software Engineering, SE-7(4):417–426, July 1981.CrossRefMathSciNetGoogle Scholar
  19. [Pnu85]
    Amir Pnueli. In Transition From Global to Modular Temporal Reasoning about Programs. In Krzysztof R. Apt, editor, NATO ASI Series, volume F13, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Ralf Pinger
    • 1
  • Hans-Dieter Ehrich
    • 1
  1. 1.Abteilung InformationssystemeTechnische Universität BraunschweigBraunschweigGermany

Personalised recommendations