Synthesizing Modal Transition Systems from Triggered Scenarios

Abstract

Synthesis of operational behaviour models from scenario-based specifications has been extensively studied. Focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts which provides expressive constructs for conditional universal scenarios and some limited support for non-conditional existential scenarios. In this paper we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behaviour models, such as Labelled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems, an extension of Labelled Transition Systems that can distinguish between required, unknown and proscribed behaviour to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behaviour models through refinement, which complements an incremental elicitation process suitable for specifying behaviour with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterise all the Labelled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis and Modal Transition Systems supports behaviour model elaboration.