Correct composition in the presence of behavioural conflicts and dephasing

Scenarios of execution are commonly used to specify partial behaviour and interactions between different objects and components in a system. To avoid overall inconsistency in specifications, various automated methods have emerged in the literature to compose scenario-based models. In recent work, we have shown how the theorem prover Isabelle/HOL can be combined with an SMT solver to detect inconsistencies between sequence diagrams and, only in their absence, generate the behavioural composition. In this paper, we exploit this combination further and present an efficient approach that generates all valid composed traces giving us an equivalent representation of the conflict-free valid composed model. In addition, we show a novel way to prove the correctness of the computed results, and compare this method with the implementation and verification done within Isabelle alone. To reduce the complexity of our technique, we consider priority constraints and a notion of dephased models, i.e., models which start execution at different times. This work has been inspired by a problem from a medical domain where different clinical guidelines for chronic conditions may be applied to the same patient at different points in time. We illustrate the approach with a realistic example from this domain.