Abhik Roychoudhury
Ankit Goel
ABSTRACT
Message Sequence Charts (MSCs) are a widely used visual formalism for scenario-based specifications of distributed reactive systems. In its conventional usage, an MSC captures an interaction snippet between concrete objects in the system. This leads to voluminous specifications when the system contains several objectsthat are behaviorally similar. In this paper, we propose a lightweight syntactic and semantic extension of MSCs, called Symbolic MSCs or SMSCs, where an MSC lifeline can denote some/all objects from a collection. Our extensions give us substantially more modeling power. Moreover, we present a symbolic execution semantics for (structured collections of) our extended MSCs. This allows us to validate MSC-based system models capturing interactions between large, or even unbounded, number of objects. Since our extensions are only concerned with MSC lifelines, we believe that they can be integrated into existing standards such as UML 2.0.
- ITU-TS Recommendation Z.120, 1996. Message Sequence Charts (MSC).Google Scholar
- M. A. Reniers. Message Sequence Chart: Syntax and Semantics. PhD thesis, Technical University Eindhoven, 1999.Google Scholar
- H. Storrle. Semantics of interactions in UML 2.0. In Visual Languages and Formal Methods (VLFM), 2003.Google ScholarCross Ref
- Center-TRACON Automation System (CTAS) for air traffic control. http://ctas.arc.nasa.gov/.Google Scholar
- I. Kruger, W. Prenninger, and R. Sander. Broadcast MSCs. Formal Aspects of Computing, 16(3), 2004. Google ScholarCross Ref
- CTAS requirements document. http://scesm04.upb.de/case-study-2/requirements.pdf/.Google Scholar
- M. R. Mousavi, M. A. Reniers, and J. F. Groote. Congruence for SOS with data. In LICS, 2004. Google ScholarDigital Library
- A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,infinity)-counter abstraction. In CAV, 2002. Google ScholarDigital Library
- XSB logic programming system. http://xsb.sourceforge.net/.Google Scholar
- A. Goel, S. Meng, A. Roychoudhury, and P. S. Thiagarajan. Interacting process classes. In ICSE, 2006. Google ScholarDigital Library
- B. Genest, M. Minea, A. Muscholl, and D. Peled. Specifying and verifying partial order properties using template MSCs. In FOSSACS, 2004.Google ScholarCross Ref
- B. Sengupta and R. Cleaveland. Triggered message sequence charts. In FSE, 2002. Google ScholarDigital Library
- W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 2001. Google ScholarDigital Library
- S. Uchitel, J. Kramer, and J. Magee. Negative scenarios for implied scenario elicitation. In FSE, 2002. Google ScholarDigital Library
- D. Harel and R. Marelly. Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag, 2003. Google ScholarDigital Library
Index Terms
- Symbolic message sequence charts
Recommendations
Triggered message sequence charts
We propose an extension to Message Sequence Charts called Triggered Message Sequence Charts (TMSCs) that are intended to capture system specifications involving nondeterminism in the form of conditional scenarios. The visual syntax of TMSCs closely ...
Symbolic Message Sequence Charts
Message sequence charts (MSCs) are a widely used visual formalism for scenario-based specifications of distributed reactive systems. In its conventional usage, an MSC captures an interaction snippet between concrete objects in the system. This leads to ...
Triggered Message Sequence Charts
This paper introduces Triggered Message Sequence Charts (TMSCs), a graphical, mathematically well-founded framework for capturing scenario-based system requirements of distributed systems. Like Message Sequence Charts (MSCs), TMSCs are graphical ...
Comments