Composing specifications

ABSTRACT

A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 2: Martín Abadi , Leslie Lamport , Pierre Wolper, Realizable and Unrealizable Specifications of Reactive Systems, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.1-17, July 11-15, 1989
• 3: ALPERN, B., AND SCHNEIDER, F B. Defining likeness, Inf. Process. Lett 21, 4 (Oct. 1985), 181-185.
• 4: APT, K R, FRANCEZ, N., AND KATZ, S. Appraising fairness in languages for distributed programming. Dtstrtbuted Comput 2 (1988), 226-241.
• 5: Howard Barringer , Ruurd Kuiper , Amir Pnueli, A really abstract concurrent model and its temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.173-183, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512660]
• 6: BROY, M , DEDERICHS, F , DENDORFER, C , AND WEBER, R. Characterizing the behaviour of reactive systems by trace sets. In 3rd workshop on Concurrency and Compositionality (Saint Augustin, Germany, 1991), E, Best and G Rozenberg, Eds., vol. 191 of GMD-Studien, GMD, pp. 47-56 Extended abstract.
• 7: Davis, M. Infinite games of perfect reformation. In Advances in Game Theory, M. Dresher, L, S. Shapley, and A. W. Tucker, Eds,, vol. 52 of Annals of Mathematics Studtes. Princeton University Press, Princeton, N. J., 1964, pp. 85-101,
• 8: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, 1987
• 9: D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 10: HOARE, C A. R. Proof of correctness of data representations. Acts Inf. 1 (1972), 271-281.
• 11: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 12: LANI, S S , AND SHANKAR, A U Protocol verification via projections. AEE A Trans on Softw. Eng SE-10, 4 (July 1984), 325-342.
• 13: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 14: LAMPORT, L What good is temporal logic? In Information Processing 83; Proceedings of the IFIP 9th World Congress (Paris, Sept. 1983), R. E A. Mason, Ed., IFIP, North Holland, pp. 657-668.
• 15: Leslie Lamport, 1983 Invited address solved problems, unsolved problems and non-problems in concurrency, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.1-11, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806731]
• 16: Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989 [doi>10.1145/63238.63240]
• 17: LAMPORT, L The temporal logic of ac'uons. Research report 79, Digital Equipment Corporation, Systems Research Center, Dec. 1991.
• 18: Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984 [doi>10.1145/2993.357247]
• 19: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 20: Z Manna , Amir Pnueli, A Hierarchy of Temporal Properties, Stanford University, Stanford, CA, 1987
• 21: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 22: MISRA, J , AND CHANDY, K. M. Proofs of networks of processes. IEEE Trans. on Softw. Eng. SE-7, 4 (July 1981), 417-426.
• 23: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 24: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 25: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 26: STARK, E W Foundations of a Theory of Specification for Distributed Systems Ph D, thesis, M I T , Aug. 1984
• 27: Eugene W. Stark, A Proof Technique for Rely/Guarantee Properties, Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, p.369-391, December 16-18, 1985

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Theory, Verification

Keywords:
compositionality, concurrent programming, liveness properties, modular specification, safety properties