Modeling and verification of a telecommunication application using live sequence charts and the Play-Engine tool |
| |
Authors: | Pierre Combes David Harel Hillel Kugler |
| |
Affiliation: | (1) France Telecom Research and Development, Paris, France;(2) The Weizmann Institute of Science, Rehovot, Israel;(3) Microsoft Research, Cambridge, UK |
| |
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, . 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.
|
| |
Keywords: | Live sequence charts (LSCs) Requirements engineering Verification Telecommunication |
本文献已被 SpringerLink 等数据库收录! |
|