ECEASST Improving Live Sequence Chart to Automata Transformation for Verification

Abstract: This paper presents a Live Sequence Chart (LSC) to automata trans-formation algorithm that enables the verification of communication protocol imple-mentations. Using this LSC to automata transformation a communication protocol implementation can be verified using a single verification run as opposed to pre-vious 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 trans-formation 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