Specification and Verification of Message Sequence Charts

摘要: The use of message sequence charts (MSCs) is popular in designing and documenting communication protocols. A recent surge interest MSCs has led to various algorithms for their automatic analysis, e.g., finding race conditions. In this paper we adopt a causality based temporal logic specify properties MSCs. This alleviates some problems that arise when specifying using the traditional interleaving-based linear logic: systems are not necessarily finite state systems, leading undecidability LTL model checking. Even dealing with MSC set linearizations can easily generate an exponential space explosion. We provide efficient checking algorithm Our construction models FIFO restricted version w-automata two successor relations. implemented environment as extension SPIN system.