Abstract
This paper illustrates the use of priorities in process algebras by a real-world example dealing with the design of a safety-critical network which is part of a railway signaling system. Priorities in process algebras support an intuitive modeling of distributed systems since undesired inter-leavings can be suppressed. This fact also leads to a substantial reduction of the sizes of models. We have implemented a CCS-based process algebra with priorities as a new front-end for the NCSU Concurrency Workbench, and we use model checking for verifying properties of the signaling system.
Research supported by NSF/DARPA grant OCR-9014775, NSF grant CCR-9120995, ONR Young Investigator Award N00014-92-J-1582, NSF Young Investigator Award CCR-9257963, NSF grant CCR-9402807, and AFOSR grant F49620-95-1-0508.
Research support for the second author provided by the German Academic Exchange Service under grant D/95/09026 (Doktorandenstipendium HSP II / AUFE).
Chapter PDF
References
J. Baeten, editor. Applications of Process Algebra, volume 17 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, England, 1990.
J. Baeten, J. Bergstra, and J. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae IX, pages 127–168, 1986.
G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal Μ-calculus. To appear in Proceedings of Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), 1996.
T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14:25–59, 1987.
G. Bruns. A case study in safety-critical design. In G. Bochmann and D. Probst, editors, Computer Aided Verification (CAV '92), volume 663 of Lecture Notes in Computer Science, pages 220–233, Montréal, June/July 1992. Springer-Verlag.
J. Camilleri and G. Winskel. CCS with priority choice. In Sixth Annual Symposium on Logic in Computer Science (LICS '91), pages 246–255, Amsterdam, July 1991. IEEE Computer Society Press.
R. Cleaveland. Analyzing concurrent systems using the Concurrency Workbench. In P. Lauer, editor, Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693 of Lecture Notes in Computer Science, pages 129–144. Springer-Verlag, 1993.
R. Cleaveland and M. Hennessy. Priorities in process algebra. Information and Computation, 87(1/2):58–77, July/August 1990.
R. Cleaveland, E. Madelaine, and S. Sims. Generating front-ends for verification tools. In E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '95), volume 1019 of Lecture Notes in Computer Science, pages 153–173, Aarhus, Denmark, May 1995. Springer-Verlag.
R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics-based tool for the verification of finite-state systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, January 1993.
A. Cribbens. Solid-state interlocking (SSI): an integrated electronic signalling system for mainline railways. IEE Proceedings, 134, Pt. B(3), May 1987.
D. Kozen. Results on the propositional Μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
R. Milner. Communication and Concurrency. Prentice-Hall, London, 1989.
V. Natarajan, L. Christoff, I. Christoff, and R. Cleaveland. Priorities and abstraction in process algebra. In P. Thiagarajan, editor, Foundations of Software Technology and Theoretical Computer Science, volume 880 of Lecture Notes in Computer Science, pages 217–230, Madras, India, Dec. 1994. Springer-Verlag.
W. Yi. CCS + time = an interleaving model for real time systems. In J. L. Albert, B. Monien, and M. R. Artalejo, editors, Automata, Languages and Programming (ICALP '91), volume 510 of Lecture Notes in Computer Science, pages 217–228, Madrid, July 1991. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cleaveland, R., Lüttgen, G., Natarajan, V., Sims, S. (1996). Priorities for modeling and verifying distributed systems. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_50
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive