Towards automated verification of Splice in muCRL
P. F. G. Dechering, Izak van Langevelde · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2000
A considerable fragment of the coordination architecture Splice, including Ethernet, is specified in the process-algebraic language crl. This specification is used to generate transition systems for a number of simple Splice applications which are verified by model checking using the Caesar/Ald' ebaran tool set. For these cases the properties of deadlock freeness, soundness and weak completeness are proven. The primary result reported is a detailed formal model of Splice that makes possible automated verification. In practice, however, it is only for very simple Splice applications feasible to generate a transition system. Nevertheless, model checking applied to a large number of small applications, or scenarios, can be used to gather evidence for the validity of properties that is more general than testing in that it considers all possible system traces for a given scenario instead of just one trace. For applications with a high degree of non-determinism this can be an interesting adv...