Abstract
This paper is about specification and verification of processes, modeled as CCSagents.We show, by means of examples that Hennessy-Milner Logic (HML) with recursion is a suitable language for expressing implicit specifications. By extending this specification language with refinement operators, i.e. operators that describe the internal structure of a system, we obtain a calculus for stepwise refinement of agents from a specification in HML to a realization in CCS. The method is demonstrated by proving the alternating-bit protocol under weak assumptions about the unreliable media.
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
S. Brookes and W. Rounds, Behavioural equivalences induced by programming logics, ICALP’83, LNCS 154, 1983.
S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS, ICALP’84, LNCS 172.
M. Hennessy and R. Milner, Algebraic laws for Nondeterminism and Concurrency, JACM 32 (1), (1985).
D. Kozen, Results on the Propositional µ-calculus, ICALP’82, LNCS 140.
K.G. Larsen, Context-Dependent Bisimulation between processes, Ph. D. thesis CST 37–86, University of Edinburgh, 1986.
K. G. Larsen and R. Milner, A Complete Protocol Verification using Relativized Bisimulation, R 86–12, Institute of Electronic Systems, Aalborg University Center.
K.G. Larsen, Proof Systems for Hennessy-Milner Logic with Recursion, to appear in CAAP’88.
R. Milner, A Calculus of Communicating Systems, LNCS 92.
R. Milner, Calculi for Synchrony and Asynchrony, Theoretical Computer Science 25 (1983) 267–310.
R. Milner, The calculus CCS and its evaluation rules, Seminar on Concurrency, CMU, LNCS 197.
G. Winskel, A Complete Proof System for SCCS with Modal Assertions, Cambridge Computer Lab., Techn. Rep. 78, September 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer-Verlag London
About this paper
Cite this paper
Holmström, S. (1990). Hennessy-Milner Logic with recursion as a specification language, and a refinement calculus based on it. In: Rattray, C. (eds) Specification and Verification of Concurrent Systems. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3534-0_15
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3534-0_15
Publisher Name: Springer, London
Print ISBN: 978-3-540-19581-8
Online ISBN: 978-1-4471-3534-0
eBook Packages: Springer Book Archive