Constructing comprehensive operational models of intended system behavior is a complex and costly task, which can be mitigated by the construction of partial behavior models, providing early feedback and subsequently elaborating them iteratively. However, how should partial behavior models with different viewpoints covering different aspects of behavior be composed? How should partial models of component instances of the same type be put together? In this article, we propose model merging of modal transition systems (MTSs) as a solution to these questions. MTS models are a natural extension of labelled transition systems that support explicit modeling of what is currently unknown about system behavior. We formally define model merging based on weak alphabet refinement, which guarantees property preservation, and show that merging consistent models is a process that should result in a minimal common weak alphabet refinement (MCR). In this article, we provide theoretical results and algorithms that support such a process. Finally, because in practice MTS merging is likely to be combined with other operations over MTSs such as parallel composition, we also study the algebraic properties of merging and apply these, together with the algorithms that support MTS merging, in a case study.

Synthesis of behavior models from software development artifacts such as scenario-based descriptions or requirements specifications helps reduce the effort of model construction. However, the models favored by existing synthesis approaches are not sufficiently expressive to describe both universal constraints provided by requirements and existential statements provided by scenarios. In this paper, we propose a novel synthesis technique that constructs behavior models in the form of modal transition systems (MTS) from a combination of safety properties and scenarios. MTSs distinguish required, possible, and proscribed behavior, and their elaboration not only guarantees the preservation of the properties and scenarios used for synthesis but also supports further elicitation of new requirements.

Synthesis of behaviour models from software development artifacts such as scenario-based descriptions or requirements specifications not only helps significantly reduce the effort of model construction, but also provides a bridge between approaches geared toward requirements analysis and those geared towards reasoning about system design at the architectural level. However, the models favoured by existing synthesis approaches are not sufficiently expressive to describe both universal constraints provided by requirements and existential statements provided by scenarios. In this paper, we propose a novel synthesis technique that constructs behaviour models in the form of modal transition systems (MTS) from a combination of safety properties and scenarios. MTSs distinguish required, possible and proscribed behaviour, and their elaboration not only guarantees the preservation of the properties and scenarios used for synthesis but also supports further elicitation of new requirements.