Improving Live Sequence Chart to Automata Transformation for Verification

  • 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 fromThis 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.show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author: Rahul Kumar, Eric G Mercer
URN:urn:nbn:de:kobv:83-opus-19843
ISBN:1863-2122
Series (Serial Number):Electronic Communications of the EASST- ECEASST (10/04)
Document Type:Arbeitspapier/Research Paper
Language:English
Date of Publication (online):2008/08/28
Publishing Institution:Technische Universität Berlin
Release Date:2008/08/28
Tag:Graph Transformation; automata; live sequence chart; transformation; verification
Note:
http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/19
Institutes:Institut für Softwaretechnik und Theoretische Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Collection:Volume 10 (2008): Graph Transformation and Visual Modeling Techniques 2008
Licence (German):License LogoCC BY-NC-SA 2.0 DE: Creative Commons-Lizenz: Namensnennung, nicht kommerziell, Weitergabe unter gleichen Bedingungen 2.0 Deutschland