Synthesis of behavioral models from scenarios
| Autor: | Jeff Kramer, Jeff Magee, Sebastian Uchitel |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
Model checking
Semantics (computer science) Programming language Computer science Software requirements specification System requirements specification Specification language Reuse computer.software_genre Language Of Temporal Ordering Specification Component (UML) Formal specification computer Requirements analysis Software |
| Zdroj: | IEEE Transactions on Software Engineering. 29:99-115 |
| ISSN: | 0098-5589 |
| Popis: | Scenario-based specifications such as Message Sequence Charts (MSCs) are useful as part of a requirements specification. A scenario is a partial story, describing how system components, the environment, and users work concurrently and interact in order to provide system level functionality. Scenarios need to be combined to provide a more complete description of system behavior. Consequently, scenario synthesis is central to the effective use of scenario descriptions. How should a set of scenarios be interpreted? How do they relate to one another? What is the underlying semantics? What assumptions are made when synthesizing behavior models from multiple scenarios? In this paper, we present an approach to scenario synthesis based on a clear sound semantics, which can support and integrate many of the existing approaches to scenario synthesis. The contributions of the paper are threefold. We first define an MSC language with sound abstract semantics in terms of labeled transition systems and parallel composition. The language integrates existing approaches based on scenario composition by using high-level MSCs (hMSCs) and those based on state identification by introducing explicit component state labeling. This combination allows stakeholders to break up scenario specifications into manageable parts and reuse scenarios using hMCSs; it also allows them to introduce additional domain-specific information and general assumptions explicitly into the scenario specification using state labels. Second, we provide a sound synthesis algorithm which translates scenarios into a behavioral specification in the form of Finite Sequential Processes. This specification can be analyzed with the Labeled Transition System Analyzer using model checking and animation. Finally, we demonstrate how many of the assumptions embedded in existing synthesis approaches can be made explicit and modeled in our approach. Thus, we provide the basis for a common approach to scenario-based specification, synthesis, and analysis. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|