Properties of Behavioural Model Merging

Abstract

Constructing comprehensive operational models of intended system behaviour is a complex and costly task. Consequently, practitioners adopt techniques that support partial behaviour decription such as scenario-based specifications, and focus on elaborating these descriptions iteratively. In previous work, we show how this process can be formally supported by Modal Transition Systems (MTSs), observational refinement, and model merging. In this paper, we study a number of properties of merging MTSs and give insights on the implications these results have on engineering and reasoning about behaviour models. We illustrate the utility of our results on a case study.