Towards Automated Verification of SPLICE in (mu)CRL. Software Engineering

摘要

A considerable fragment of the coordination architecture SPLICE, includingETHERNET, is specified in the process-algebraic language microCRL. This specification is used to generate transition systems for a number of simple SPLICE applications which are verified by model checking using the CAESAR/ALDEBARAN 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. Nevertheless, model checking applied to a large number of small 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.