Cited By
View all- Sengupta BCleaveland R(2006)Triggered Message Sequence ChartsIEEE Transactions on Software Engineering10.1109/TSE.2006.8232:8(587-607)Online publication date: 1-Aug-2006
Executable requirements specifications using triggered message sequence charts
Pages 482 - 493
Abstract
Triggered Message Sequence Charts (TMSCs) are a scenario-based visual formalism for early stage requirements specifications of distributed systems. In this paper, we present a formal operational semantics for TMSCs that allow the simulation of TMSC system descriptions, so that errors and inconsistencies in specification may be detected early on. The semantics is defined in terms of Structured Operational Semantics (SOS) rules that guide the step-wise execution of TMSC specifications. We also consider the equivalence of this semantics and the TMSC denotational semantics that has been presented in previous work.
References
[1]
Message sequence charts (MSC). ITU-TS Recommendation Z.120, 1996.
[2]
R. Alur, G. J. Holzmann, and D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70-77, 1996.
[3]
H. Ben-Abdallah and S. Leue. MESA: Support for scenario-based design of concurrent systems. Proc. of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, LNCS volume 1384:118-135.
[4]
B.Sengupta and R.Cleaveland. TRIM: A tool for triggered message sequence charts. Proceedings of 15TH Computer Aided Verification Conference (CAV'03) (tool paper), 2003.
[5]
W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1), 2001.
[6]
D.Harel and R.Marelly. Specifying and executing behavioral requirements: The play-in/ play-out approach. Software and System Modeling (SoSym), 2003.
[7]
G.Plotkin. A structural approach to operational semantics. Technical report, University of Aarhus, Denmark, 1981.
[8]
M. Hennessy. Algebraic theory of processes. The MIT Press, 1988.
[9]
I. Kruger. Distributed system design with message sequence charts. PhD Thesis, Technical University of Munich, 2000.
[10]
R.Cleaveland and S.Sims. The ncsu concurrency workbench. Computer Aided Verification (CAV), 1996, LNCS volume 1102:394-397.
[11]
M. A. Reniers. Message sequence chart: Syntax and semantics. PhD Thesis, Eindhoven University of Technology, 1998.
[12]
B. Sengupta and R. Cleaveland. Refinement-based requirements modeling using triggered message sequence charts. 11th IEEE Int'l Requirements Engineering Conference, 2003.
[13]
B. Sengupta and R. Cleaveland. Triggered message sequence charts. ACM SIGSOFT 2002, 10th Int'l Symposium on the Foundations of Software Engineering (FSE-10), pages 167-176.
[14]
J.Kramer S.Uchitel and J.Magee. Ltsa-msc: Tool support for behaviour model elaboration using implied scenarios. TACAS'03.
[15]
T.Wang, A.Roychoudhury, R.Yap, and S.C.Choudhary. Symbolic execution of behavioral requirements. PADL 2004, LNCS vol. 3057.
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 ...
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
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 22 December 2005
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 21 Nov 2024
Other Metrics
Citations
Cited By
View all- Sengupta BCleaveland R(2006)Triggered Message Sequence ChartsIEEE Transactions on Software Engineering10.1109/TSE.2006.8232:8(587-607)Online publication date: 1-Aug-2006
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in