Abstract
The growing popularity of sequence charts, first of all Message Sequence Charts and UML Sequence Diagrams, for the description of communication behavior has evoked criticism regarding the semantics of the charts which led to extensions of these standardized visual formalisms. One such extension are Live Sequence Charts which allow to distinguish mandatory and possible behavior in protocol specifications. In the original language definition for LSCs the semantics are only described informally, although a sketch for a possible formalization has been provided as well. In this paper we intend to fill in the semantic blanks of the original LSCde finition. Following the sketched path we define the semantics of an LSCb y deriving a Timed Büchi Automata from it. We also consider qualitative and quantative timing aspects. We finally show how LSCs are integrated into a verification tool set for Statemate designs.
Research in part supported by the German Research Council (DFG) within the USE project as part of the SPP Integration of Specification Techniques with Engineering Applications
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. Dill. The Theory of Timed Automata. In de Bakker, Henzinger, and de Roever, editors, Proceedings of Rex 1991: Real Time in Theory and Practice, number 600 in LNCS. Springer Verlag, 1992.
R. Alur, G. J. Holzmann, and D. Peled. An analyzer for Message Sequence Charts. In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of Lecture Notes in Computer Science, pages 35–48, Passau, Germany, 1996. Springer-Verlag.
R. Alur. Timed Automata. In NATO-ASI 1998 Summer School on Verification of Digital and Hybrid Systems, 1998.
Tom Bienmüller, Udo Brockmeyer, and Werner Damm et. al. Formal Verification of an Avionics Application using Abstraction and Symbolic Model Checking. In Felix Redmill and Tom Anderson, editors, Towards System Safety-Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK, pages 150–173. Safety-Critical Systems Club, Springer-Verlag, 1999.
W. Damm, G. Döhmen, and J. Klose. Secure Decentralized Control of Railway Crossings. In S. Gnesi and D. Latella, editors, Fourth International ERCIM Workshop on Formal Methods in Industrial Critical Systems, 1999.
W. Damm and D. Harel. LSCs: Breathing Life into Message Sequence Charts. In FMOODS’99 IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems, 1999.
W. Damm and D. Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 2001. to appear.
Werner Damm and Jochen Klose. Verification of a Radio-based Signaling System Using the Statemate Verification Environment. Formal Methods in System Design, 2001. to appear.
Konrad Feyerabend. Realtime Symbolic Timing Diagrams. Technical report, Carl von Ossietzky Universität Oldenburg, 1996.
Konrad Feyerabend and Bernhard Josko. A visual formalism for real time requirement specifications. In Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrentand Distributed Software, ARTS’97, Lecture Notes in Computer Science 1231, pages 156–168, 1997.
David Harel and Michal Politi. Modeling Reactive Systems with Statecharts: The STATEMATE Approach. Part No. D-1100-43. i-Logix Inc., Three Riverside Drive, Andover, MA 01810, June 1996.
ITU-T. ITU-T Annex B to Recommendation Z.120 Formal Semantics of Message Sequence Charts. ITU-T, Geneva, 1996.
ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva, October 1996.
Ingolf Krüger. Towards the Methodical Usage of Message Sequence Charts. In Katharina Spies and Bernhard Schätz, editors, Formale Beschreibungstechniken für verteilte Systeme (FBT99), 9. GI/ITG Fachgespräch, pages 123–134. Herbert Utz Verlag, June 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klose, J., Wittke, H. (2001). An Automata Based Interpretation of Live Sequence Charts. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_35
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive