Improving Live Sequence Chart to Automata Transformation for Verification

Abstract

This paper presents a Live Sequence Chart (LSC) to automata
transformation algorithm that enables the verification of
communication protocol implementations. Using this LSC to automata
transformation a communication protocol implementation can be verified
using a single verification run as opposed to previous techniques that
rely on a three stage verification approach. The novelty and
simplicity of the transformation algorithm lies in its placement of
accept states in the automata generated from the LSC. We present in
detail an example of the transformation as well as the transformation
algorithm. Further, we present a detailed analysis and an empirical
study comparing the verification strategy to earlier work to show the
benefits of the improved transformation algorithm.