Structured operational semantics as a specification language

ABSTRACT

Standard specification languages have very limited abilities to define new operations on processes. We introduce the concept of a Protean specification language, with general definitional facilities supported by the appropriate theory. Protean languages allow elegant, readable, and useful specifications at all levels of abstraction. A good Protean specification language will admit methods of verifying that one specification is a refinement of another. We sketch a family of Protean specification languages (with references to the full details) which allow a vast amount of expressive power in defining operations, but nonetheless have all the essential theoretical and specification power of CCS and ACP.We illustrate these techniques by presenting several specifications of the job of protecting an arbitrary server by a checkpoint/backup scheme. The high-level specification of the protected server simply says, “It does everything it did before, and it doesn't crash.” The middle-level specification describes checkpointing cleanly and abstractly, without prescribing any particular implementation. The low-level specification is fairly close to an implementation. We show the high- and medium-level specifications equivalent by bisimulation relation techniques, and the medium- and low-level specifications equivalent by equational reasoning using automatically-generated equations. We also show that the operations expressing checkpointing behavior are not definable in standard process algebras.

REFERENCES

• Abr87: S. Abramsky, Observation equivalence as a testing equivalence, Theoretical Computer Science, v.53 n.2-3, p.225-241, Aug. 1987 [doi>10.1016/0304-3975(87)90065-X]
• ABV92: Luca Aceto, Bard Bloom, and Frits Vaandrager. Turning SOS rules into equations. In Proceedings of LICS '92, pages 113-124. IEEE Computer Society Press, 1992.
• AL91: Martín Abadi , Leslie Lamport, An Old-Fashioned Recipe for Real Time, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.1-27, June 03-07, 1991
• Bae90: J. C. M. Baeten, Applications of process algebra, Cambridge University Press, New York, NY, 1990
• BB87: Tommaso Bolognesi , Ed Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, v.14 n.1, p.25-59, March, 1987 [doi>10.1016/0169-7552(87)90085-7]
• BIM88: B. Bloom , S. Istrail , A. R. Meyer, Bisimulation can't be traced, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.229-239, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73580]
• BK92: Bard Bloom , Marta Z. Kwiatkowska, Trade-Offs in True Concurrency: Pomsets and Mazurkiewicz Traces, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.350-375, March 25-28, 1991
• Blo89: Bard Bloom. Ready Simulation, Bisimulation, and the Semantics of CCS-Like Languages. PhD thesis, Massachusetts Institute of Technology, August 1989.
• Blo93: Bard Bloom, Structural Operational Semantics for Weak Bisimulations, Cornell University, Ithaca, NY, 1993
• BM92: Bard Bloom , Albert R. Meyer, Experimenting with process equivalence, Theoretical Computer Science, v.101 n.2, p.223-237, July 20, 1992 [doi>10.1016/0304-3975(92)90050-P]
• BW90: J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
• Hoa85: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• LT87: 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]
• Luc90: David C. Luckham, Programming with Specifications: An Introduction to Anna, a Language for Specifying ADA Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1990
• Mil81: Robin Milner, A Modal Characterisation of Observable Machine-Behaviour, Proceedings of the 6th Colloquium on Trees in Algebra and Programming, p.25-34, March 05-07, 1981
• Mil89: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• MP83: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• PP88: G.D. Plotkin and V.R. Pratt. Teams can see pomsets. Manuscript available as pub/pp.tex by anonymous FTP from Boole.Stanford.EDU, October 1988.
• vG93: Rob J. van Glabbeek, The Linear Time - Branching Time Spectrum II, Proceedings of the 4th International Conference on Concurrency Theory, p.66-81, August 23-26, 1993
• vGW89: Rob van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. In G. X. Ritter, editor, Information Processing 89: Proceedings of the IFIP 11th World Computer Congress, pages 613-618. North-Holland, August 1989. TUM report I9052 (- SFB-Bericht Nr. 342/29/90 A) and CWI report CS-R9120.
• WBB92: Sam Weber, Bard Bloom, and Geoffrey Brown. Compiling Joy to silicon: A verified silicon compilation scheme. In Tom Knight and John Savage, editors, Proceedings of the Advanced Research in VLSI and Parallel Systems Conference, pages 79- 98. 1992.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Algorithms, Languages, Theory, Verification