Abstract
Process calculi are commonly used to specify and verify communication protocols. Once verified, it is desirable to be able to implement a protocol or other concurrent design using automatic assistance and in a provably correct way. Previously, the author has introduced a representation for a process calculus program in the form of a graph with parameters. A formally proved mapping from CCS programs to this representation has also been presented. Here we present a translation from the representation to a subset of C which has a formal semantics. The translation is formally defined and proved correct (the proof is not included here but is presented in [14]). While other work has already been done on such translations, this is the first translation with a correctness proof, therefore being more in the spirit of formal methods. Further, we introduce a flexible approach to resolving non-determinism which gives this translation a practical advantage.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Computation, 60: 109–137, 1984.
T. Bolognesi and E. Brinksma Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14: 22–59, 1987.
G. Bruns. A language for value-passing CCS. Technical Report ECS-LFCS-91–175, LFCS, Dept of Computer Science, University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, August 1991.
L. Cardelli and R. Pike. Squeak: a language for communicating with mice. In ACM SIGRAHP, volume 19, number 3, pages 199–204, July 1985.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
G. Karjoth. XFSM: A formal model of communicating state machines for implementing specifications. Technical Report RZ 2209 (#75693), IBM Research Division, 09/12/91.
G. Karjoth. Implementing process algebra specifications by state machines. In Protocol Specification, Testing, and Verification, VIII, pages 47–62. IFIP, 1988.
B. W. Kernighan and D. M. Ritchie. The C Programming Language. Prentice-Hall, Englewood Cliffs, New Jersey 07632, 2nd edition, 1988.
J. A. Manas and T. de Miguel. From LOTOS to C. In K. Turner, editor, Formal Description Techniques I, pages 79–84. North-Holland, 1988.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons Ltd., Baffin Lane, Chichester, West Sussex P019 IUD, England, 1992.
G. D. Plotkin. A Structural Approach to Operational Semantics. Computer Science Dept, Aarhus University, September 1981.
Z. Schreiber. Verification and analysis of value-passing CCS programs with infinite sorts. Technical Report DoC 92/9, Department of Computing, Imperial College, 180 Queen’s Gate, London SW7 2BZ, June 1992.
Z. Schreiber. Implementing process algebra in C. Technical Report DoC 93/5, Department of Computing, Imperial College, 180 Queen’s Gate, London SW7 2BZ, June 1993.
P. van Eijk, H. Kremer, and M. van Sinderen. On the use of specification styles for automated protocol implementation from LOTOS to C. In Protocol Specification, Testing and Verification, X, pages 157–168. IFIP, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 British Computer Society
About this paper
Cite this paper
Schreiber, Z. (1993). Implementing Process Calculi in C. In: Burn, G., Gay, S., Ryan, M. (eds) Theory and Formal Methods 1993. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3503-6_23
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3503-6_23
Publisher Name: Springer, London
Print ISBN: 978-3-540-19842-0
Online ISBN: 978-1-4471-3503-6
eBook Packages: Springer Book Archive