Abstract
We apply the language of live sequence charts (LSCs) and the Play-Engine tool to a real-world complex telecommunication service. The service, called Depannage, allows a user to make a phone call and ask for help from a doctor, the fire brigade, a car maintenance service, etc. This kind of service is built on top of an embedded platform, using both new and existing service components. The complexity of such applications stems from their distributed architecture, the various time constraints they entail, and the fact the underlying systems are rapidly evolving, introducing new components, protocols and associated hardware constraints, all of which must be taken into account. We present the results of our work on the specification, animation and formal verification of the Depannage service, and draw some initial conclusions as to an appropriate methodology for using a scenario-based approach in the telecommunication domain. The complete specification of the Depannage application in LSCs and some animations showing simulation and verification results are made available as supplementary material.
This research was supported by the European Commission project OMEGA (IST-2001-33522).
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
Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)
Castanet, R., Cavalli, A., Combes, P., Laurencot, P., MacKaya, M., Mederreg, A., Monin, W., Zaidi, F.: A multi-service and multi-protocol validation platform-experimentation results. In: Groz, R., Hierons, R.M. (eds.) TestCom 2004. LNCS, vol. 2978, pp. 17–32. Springer, Heidelberg (2004)
Combes, P., Dubois, F., Monin, W., Vincent, D.: Looking for better integration of design and performance engineering. In: Reed, R. (ed.) SDL 2003. LNCS, vol. 2708, pp. 1–17. Springer, Heidelberg (2003)
Combes, P., Dubois, F., Renard, B.: An Open Animation Tool: Application to Telecommunications Systems. Computer Networks 40(5), 599–620 (2002)
Combes, P., Harel, D., Kugler, H.: Supplementary material on the depannage application, http://cs.nyu.edu/~kugler/Depannage/
Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001); Preliminary version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1999)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002); Also available as Tech. Report MCS02-08, The Weizmann Institute of Science
Harel, D., Kugler, H., Weiss, G.: Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach. In: Leue, S., Systä, T.J. (eds.) Scenarios: Models, Transformations and Tools. LNCS, vol. 3466, pp. 26–42. Springer, Heidelberg (2005)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach. Software and System Modeling (SoSyM) 2(2), 82–107 (2003)
Logrippo, L., Amyot, D.: Feature Interactions in Telecommunications and Software Systems VII. IOS Press, Amsterdam (2003)
Marelly, R., Harel, D., Kugler, H.: Multiple instances and symbolic variables in executable sequence charts. In: Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2002), Seattle, WA, pp. 83–100 (2002)
ITU-TS Recommendation Z.120 (11/99): MSC 2000. ITU-TS, Geneva (1999)
UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), http://www.omg.org
Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Combes, P., Harel, D., Kugler, H. (2005). Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_31
Download citation
DOI: https://doi.org/10.1007/11562948_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)