Towards automated verification of Splice in $ mu $CRL

A considerable fragment of the coordination architecture {sc Splice, including Ethernet, is specified in the process-algebraic language{$mu${sc crl. This specification is used to generate transition systems for a number of simple{sc Splice applications which are verified by model checking using the{sc C{aesar/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{sc Splice that makes possible automated verification. In practice, however, it is only for very simple {sc 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 advantage.