Message Sequence Charts (MSCs) are used to specify the behaviour of communicating systems through scenarios. Though timing constraints are natural for describing the behaviour of real-life protocols, the basic MSC notation has no mechanism to specify such constraints. We propose a notation for specifying collections of timed scenarios and describe a framework for automatic verification of scenariobased properties for communicating finite-state machines equipped with local clocks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, G. Holzmann and D. Peled: An analyzer for message sequence charts. Software Con-cepts and Tools, 17(2) (1996) 70-77.
G. Behrmann, A. Davida and K.G. Larsen: A Tutorial on Uppaal, Proc. SFM 2004, LNCS 3185, Springer-Verlag (2004) 200-236.
J. Bengtsson and Wang Yi: Timed Automata: Semantics, Algorithms and Tools, Lectures on Concurrency and Petri Nets 2003, LNCS 3098, Springer-Verlag (2003) 87-124.
P. Chandrasekaran and M. Mukund: Matching Scenarios with Timing Constraints, Proc. FOR-MATS 2006, Springer LNCS 4202 (2006) 98-112.
W. Damm and D. Harel: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1) (2001) 45-80.
D. de Souza and M. Mukund: Checking Consistency of SDL+MSC Specifications, Proc. SPIN Workshop 2003, LNCS 2648, Springer-Verlag (2003) 151-165.
J.G. Henriksen, M. Mukund, K. Narayan Kumar, M. Sohoni and P.S. Thiagarajan: A theory of regular MSC languages. Inf. Comp., 202(1) (2005) 1-38.
G.J. Holzmann: The model checker SPIN, IEEE Trans. on Software Engineering, 23, 5 (1997) 279-295.
ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU, Geneva (1999).
P. Krcal and Wang Yi: Communicating Timed Automata: The More Synchronous, the More Difficult to Verify, CAV 2006, LNCS, Springer-Verlag (2006), 249-262.
A. Muscholl, D. Peled, and Z. Su: Deciding Properties for Message Sequence Charts. Proc. FOSSACS’98, LNCS 1378, Springer-Verlag (1998) 226-242.
Akshay Sunderaraman, Formal Specification and Verification of Timed Com-municating Systems, Master’s thesis, LSV, ENS Cachan (2006). Available at http://www.lsv. ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer
About this paper
Cite this paper
Chandrasekaran, P., Mukund, M. (2007). Adding Time to Scenarios. In: Ramesh, S., Sampath, P. (eds) Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-6254-4_7
Download citation
DOI: https://doi.org/10.1007/978-1-4020-6254-4_7
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-6253-7
Online ISBN: 978-1-4020-6254-4
eBook Packages: EngineeringEngineering (R0)