Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool

P. Combes, D. Harel, and H. Kugler

Abstract

We apply the scenario-based approach to modeling, via the language of live sequence charts (LSCs) and the Play-Engine tool to a real-world complex telecommunication service, Depannage. It allows a user to call for help from a doctor, the fire brigade, a car maintenance service, etc. These kinds of services are built on top of an embedded platform, using both new and existing service components, and their complexity stems from their distributed architecture, the various time constraints they entail, and their rapidly evolving underlying systems. A well known problem in this class of telecommunication applications is that of feature interaction, whereby a new feature might cause problems in the execution of existing features. Our approach provides a methodology for high-level modeling of telecommunication applications that can help in detecting feature interaction at early development stages. We exhibit the results of applying the methodology to the specification, animation and formal verification of the Depannage service.

Details

Publication typeArticle
Published inSoftware and Systems Modeling
URLhttp://dx.doi.org/10.1007/s10270-007-0069-5
Pages157-175
Volume7
Number2
PublisherSpringer Verlag
> Publications > Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool