Paper Info
Title
An Automata Based Interpretation of Live Sequence Charts
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 LSC definition. 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.
Year
DOI
Venue
2001
10.1007/3-540-45319-9_35
TACAS
Keywords
Field
DocType
lscb y,statemate design,live sequence charts,uml sequence diagrams,possible behavior,communication behavior,original lsc definition,original language definition,message sequence charts,possible formalization,uml sequence diagram,message sequence chart
Sequence diagram,Knowledge representation and reasoning,Computer science,Automaton,Formal specification,Theoretical computer science,Message sequence chart,Temporal logic,Semantics,Büchi automaton
Conference
ISBN
Citations 
PageRank 
3-540-41865-2
62
3.34
References 
Authors
7
2
Name
Order
Citations
PageRank
Jochen Klose115110.10
Hartmut Wittke21146.58