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.

Pdf version

Conference Slides

R. Kumar and E. G. Mercer. “Improving Live Sequence Chart to Automata Translation for Verification,” Seventh International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08), Budapest, Hungary, pp. 51 - 64, March 2008.

 @conference{kumar2007itl,
 title={Improving translation of live sequence charts to temporal logic},
 author={Kumar, R. and Mercer, E. and Bunker, A.},
 booktitle={Proc. of the 7th Int. Conf. on Automated Verification of Critical Systems (AVoCS07)},
 pages={183--197},
 year={2007}
 }