Correct Composition of Dephased Behavioural Models

TL;DR

This paper presents a method to accurately compose dephased behavioral models, ensuring consistency and correctness in complex system specifications, inspired by medical care pathway applications.

Contribution

It extends previous work by enabling the generation of correct compositions of dephased models, improving consistency checking and trace generation.

Findings

Successfully generates valid traces for dephased models

Detects inconsistencies efficiently using Isabelle and Z3

Applicable to complex, real-world scenarios like medical pathways

Abstract

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 (behavioural) models. In recent work, we have shown how the theorem prover Isabelle can be combined with the constraint solver Z3 to efficiently detect inconsistencies in two or more behavioural models and, in their absence, generate the composition. Here, we extend our approach further and show how to generate the correct composition (as a set of valid traces) of dephased models. This work has been inspired by a problem from a medical domain where different care pathways (for chronic conditions) may be applied to the same patient with different starting points.