Abstract
We consider the problem of checking whether a distributed system described in SDL is consistent with a set of MSCs that constrain the interaction between the processes. In general, the MSC constraints may be both positive and negative. The system should execute all the positive scenarios “sensibly”. On the other hand, the negative MSCs rule out some interactions as illegal. We would then like to verify that all the remaining legal interactions satisfy a desired global property, specified in linear-time temporal logic. We outline an approach to solve this problem using Spin, building in a modular way on existing tools.
Partly supported by a grant from Tata Research Development and Design Centre, Pune, India.
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 Concepts and Tools, 17(2) (1996) 70–77.
R. Alur and M. Yannakakis: Model checking of message sequence charts. Proc. CONCUR’99, LNCS 1664, Springer-Verlag (1999) 114–129.
D. Bosnacki, D. Dams, L. Holenderski and N. Sidorova: Model checking SDL with Spin, Proc TACAS 2000, LNCS 1785, Springer-Verlag (2002) 363–377.
M. Bozga, J-C. Fernandez, L. Ghirvu, S. Graf, J. P. Karimm, L. Mounier and J. Sifakis: If: An intermediate representation for SDL and its applications, Proc. SDL-FORUM’ 99, Montreal, Canada, 1999.
P. Gastin and D. Oddoux: Fast LTL to Büchi automata translation, Proc. CAV 2001, LNCS 2102, Springer-Verlag (2001) 53–65.
R. Gerth, D. Peled, M. Y. Vardi and P. Wolper: Simple on-the-fly automatic verification of linear temporal logic, Proc PSTV 95, Warsaw, Poland, Chapman & Hall (1995) 3–18.
J. G. Henriksen, M. Mukund, K. Narayan Kumar and P. S. Thiagarajan: On Message Sequence Graphs and Finitely Generated Regular MSC Languages, Proc. ICALP 2000, LNCS 1853, Springer-Verlag (2000) 675–686.
J. G. Henriksen, M. Mukund, K. Narayan Kumar and P. S. Thiagarajan: Regular Collections of Message Sequence Charts’, Proc. MFCS 2000, LNCS 1893, Springer-Verlag (2000) 405–414.
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).
ITU-T Recommendation Z.100: Specification and Description Language (SDL). ITU, Geneva (1999).
Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, Berlin (1991).
A. Muscholl, D. Peled, and Z. Su: Deciding properties for message sequence charts. Proc. FOSSACS’98, LNCS 1378, Springer-Verlag (1998) 226–242.
A. Olson et al: System Engineering using SDL-92, Elsevier, North-Holland (1997).
A. Pnueli: The Temporal Logic of Programs, Proc. 18th IEEE FOCS (1977) 46–57.
E. Rudolph, P. Graubmann and J. Grabowski: Tutorial on message sequence charts, Computer Networks and ISDN Systems—SDL and MSC, Volume 28 (1996).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
D’Souza, D., Mukund, M. (2003). Checking Consistency of SDL+MSC Specifications. In: Ball, T., Rajamani, S.K. (eds) Model Checking Software. SPIN 2003. Lecture Notes in Computer Science, vol 2648. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44829-2_10
Download citation
DOI: https://doi.org/10.1007/3-540-44829-2_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40117-9
Online ISBN: 978-3-540-44829-7
eBook Packages: Springer Book Archive