Improving Live Sequence Chart to Automata Transformation for Verification - Kumar, Rahul; Mercer, Eric (Electronic Communications of the EASST, 2008)
This paper presents a Live Sequence Chart (LSC) to automatatransformation algorithm that enables the verification ofcommunication protocol implementations. Using this LSC to automatatransformation a communication protocol implementation can be verifiedusing a single verification run as opposed to previous techniques thatrely on a three stage verification approach. The novelty andsimplicity of the transformation algorithm lies in its placement ofaccept states in the automata generated from the LSC. We present indetail an example of the transformation as well as the transformationalgorithm. Further, we present a detailed analysis and an empiricalstudy comparing the verification strategy to earlier work to show thebenefits of the improved transformation algorithm.