Scenarios describe how systems components, the environment, and various users work concurrently. Each scenario is a story, providing a partial system description, and all scenarios are combined in order to give a complete system description. Scenarios can combine unexpectedly, and some system behaviors, not present in the scenario specification, may appear in the implementation (these are called implied scenarios). Message sequence charts (MSCs) represent a very popular scenario-based language.

This paper presents an algorithm that synthesizes a labeled transition system (LTS) behavior model, which describes the implementation for a scenario-based specification such as basic MSCs and high-level MSCs, and detects the existence of implied scenarios. The investigation presented defines the closest possible implementation for a specification based on basic MSCs and high-level MSCs by extending Alur et al’s approach [1], which has been limited to a set of MSCs that specify a finite set of finite system behaviors. The framework presented integrates with existing labeled transition system analysis, and consequently the synthesized implementation can be analyzed further using model checking safety and liveness properties. It can also be animated using available tools [2].