Modeling and Verifying Distributed Systems Using Priorities: A Case Study.
Rance Cleaveland, V. Natarajan, Steve Sims, Gerald Lüttgen · 1996
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 that is part of a railway signaling system. Priorities in process algebras support an intuitive modeling of distributed systems since undesired interleavings 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 used model checking for verifying properties of the signaling system.