Search

Synthesis of operational behaviour models from scenario-based specifications has been extensively studied. Focus has been mainly on either existential or universal interpretations. Existing model synthesis techniques use traditional two-valued behaviour models such as Labeled Transition Systems (LTS). We propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. We show that LTS are not sufficiently expressive to accommodate such languages and shift the target of synthesis to Modal Transition Systems (MTS), an extension of LTS that can distinguish between required, unknown and proscribed behaviour to capture the semantics of existential and universal scenarios. MTSs 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 an MTS that uses refinement to characterise all the LTS models that satisfy a mixed, conditional existential and universal scenario-based specification. In order to capture all permissible implementations, model MTSs of component based systems are given at the system level. However, iterative refinement by engineers is often more convenient at the component level. We address the problem of decomposing partial behaviour models from a single monolithic model to a component model. We prove that a sound and complete distribution can be built when the MTS to be distributed is deterministic, transition modalities are consistent and the LTS determined by its possible transitions is distributable. We show how this combination of scenario language, synthesis, MTSs, and distribution supports behaviour model elaboration. Open Access