Synthesis and Traceability of Scenario-Based Executable Models

Message Sequence Charts (MSCs) or Sequence Diagrams are one of the behavioral diagram types in the unified modeling language or UML. In system requirements modeling, MSCs are conventionally used for describing possible system scenarios. In the recent past, there have been concerted attempts to develop executable system modeling languages directly based on MSCs - Live Sequence Charts, Triggered Message Sequence Charts and Interacting Process Classes, to name a few. In this paper, we study the problem of model synthesis in these languages - how to translate informal requirements into formal models. We also discuss (a) test generation from these formal models, and (b) how the generated tests can be traced back to the informal requirements.