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.

Modal transition systems (MTS) are operational models that distinguish between required and proscribed behaviour of the system to be and behaviour which it is not yet known whether the system should exhibit. MTS, in contrast with traditional behaviour models, support reasoning about the intended system behaviour in the presence of incomplete knowledge. In this paper, we present MTSA a tool that supports the construction, analysis and elaboration of Modal Transition Systems (MTS).

Modal Transition Systems (MTS) have been shown to be useful to reason about system behaviour in the context of partial information and to support incremental elaboration of behaviour models. A particularly useful notion in the context of software and requirements engineering is that of merge. MTS merging can be used as the conjunction of multiple partial operational descriptions which may have been provided as MTS or even synthesised from other description languages such as goal models and scenarios. One of the current limitations of MTS merging is that a complete and correct algorithm for merging has not been developed. Hence, an engineer attempting to merge partial descriptions may be prevented to do so by overconstrained algorithms or algorithms that introduce behaviour that does not follow from the partial descriptions being merged. This paper resolves these problems for strong semantics by providing a complete characterization of MTS consistency and a correct and complete algorithm for MTS merging.