Abstract
A logic and proof system is introduced for specifying and proving properties of open distributed systems. Key problems that are addressed include the verification of process networks with a changing interconnection structure, and where new processes can be continuously spawned. To demonstrate the results in a realistic setting we consider a core fragment of the Erlang programming language. Roughly this amounts to a first-order actor language with data types, buffered asynchronous communication, and dynamic process spawning. Our aim is to verify quite general properties of programs in this fragment. The specification logic extends the first-order μ-calculus with Erlang-specific primitives. For verification we use an approach which combines local model checking with facilities for compositional verification. We give a specification and verification example based on a billing agent which controls and charges for user access to a given resource.
Work partially supported by the Computer Science Laboratory of Ericsson Telecom AB, Stockholm, the Swedish National Board for Technical and Industrial Development (NUTEK) through the ASTEC competence centre, and a Swedish Foundation for Strategic Research Junior Individual Grant.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Amadio and M. Dam. A modal theory of types for the π-calculus. In Proc. FTRTFT’96, Lecture Notes in Computer Science, 1135:347–365, 1996.
G. Agha, I. A. Mason, S. F. Smith, and C. L. Talcott. A foundation for actor computation. J. Functional Programming, 7:1–72, 1997.
J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang (Second Edition). Prentice-Hall International (UK) Ltd., 1996.
M. Dam. Proving properties of dynamic process networks. To appear, Information and Computation, 1998. Preliminary version as “Compositional Proof Systems for Model Checking Infinite State Processes”, Proc. CONCUR’95, LNCS 962, pp. 12–26.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1–40 and 41–77, 1992.
D. Park. Finiteness is mu-Ineffable. Theoretical Computer Science, 3:173–181, 1976.
A. Simpson. Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 420–430, San Diego, California, 26–29 June 1995. IEEE Computer Society Press.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dam, M., Fredlund, Lå., Gurov, D. (1998). Toward Parametric Verification of Open Distributed Systems. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_7
Download citation
DOI: https://doi.org/10.1007/3-540-49213-5_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65493-3
Online ISBN: 978-3-540-49213-9
eBook Packages: Springer Book Archive