Abstract
The purpose of this paper is to present and illustrate a new compositional proof method for non-deterministic and concurrent systems; i.e. a method which allows factoring the correctness proof of a system into similar but smaller proofs of correctness of subsystems.
Our method is an extension of the well established notion of bisimulation [Par81,Mil83]; it is based on a concept of partial processes which may be related through a notion of partial bisimulation. Compared with existing methods our method has the distinct advantage of leading to simple and intuitive subspecifications without complicating the underlying theory unduly.
The method is motivated and its use illustrated through the verification of a simple scheduler.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel: A Simple Version of SCCS and Its Semantics, Unpublished notes, Edinburgh 1984.
C.A.R. Hoare, S.D. Brookes & A.W. Roscoe: A Theory of Communicating Processes, Technical Report PRG-16, Programming Research Group, University of Oxford 1981.
M. Hennessy & R. Milner: Algebraic Laws for Nondeterminism and Concurrency, Journal of the Association for Computing Machinery pp. 137–161, 1985.
C. P. Koymans & J. C. Mulder: A Modular Approach to Protocol Verification Using Process Algebra, Logic Group Preprint Series No. 6, University of Utrecht 1985.
K. G. Larsen: Context Dependent Bisimulation Between Processes, in proceedings of ICALP 85, LNCS 194, Springer Verlag 1985. Full version in TCS 49 (1987).
K. G. Larsen: Context Dependent Bisimulation Between Processes, Ph. D. Thesis, Edinburgh University 1986.
K. G. Larsen & R. Milner: Verifying a Protocol Using Relativized Bisimulation, in proceedings of ICALP 87, LNCS 267, Springer-Verlag 1987.
K. G. Larsen & B. Thomsen: A Modal Process Logic, to appear in proceedings of LICS 88.
R. Milner: A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980.
R. Milner: Calculi for Synchrony and Asynchrony, Theoretical Computer Science 25 (1983) pp 269–310, North Holland.
D. Park: Concurrency and Automata on Infinite Sequences, LNCS 104, Springer-Verlag, 1981.
G. Plotkin: A Structural Approach to Operational Semantics, DAIMI FN-19 Aarhus University Computer Science Department 1981.
R. de Simone: Higher-level Synchronising Devises in MEIJE-SCCS, TCS 37 (1985) p. 245–267.
A. Tarski: A Lattice-Theoretical Fixpoint Theorem and Its Applications, Pacific Journal of Math. 5, 1955.
B. Thomsen: An Extended Bisimulation Induced by a Preorder on Actions, M. Sc. Thesis, Aalborg University Centre 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larsen, K.G., Thomsen, B. (1988). Compositional proofs by partial specification of processes. In: Chytil, M.P., Koubek, V., Janiga, L. (eds) Mathematical Foundations of Computer Science 1988. MFCS 1988. Lecture Notes in Computer Science, vol 324. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017164
Download citation
DOI: https://doi.org/10.1007/BFb0017164
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50110-7
Online ISBN: 978-3-540-45926-2
eBook Packages: Springer Book Archive