Home > Research > Publications & Outputs > Correct composition of dephased behavioural models

Text available via DOI:

View graph of relations

Correct composition of dephased behavioural models

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published

Standard

Correct composition of dephased behavioural models. / Bowles, Juliana; Caminati, Marco B.
Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14. Vol. 10487 Springer, 2017.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Harvard

Bowles, J & Caminati, MB 2017, Correct composition of dephased behavioural models. in Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14. vol. 10487, Springer. https://doi.org/10.1007/978-3-319-68034-7_14

APA

Bowles, J., & Caminati, M. B. (2017). Correct composition of dephased behavioural models. In Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14 (Vol. 10487). Springer. https://doi.org/10.1007/978-3-319-68034-7_14

Vancouver

Bowles J, Caminati MB. Correct composition of dephased behavioural models. In Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14. Vol. 10487. Springer. 2017 doi: 10.1007/978-3-319-68034-7_14

Author

Bowles, Juliana ; Caminati, Marco B. / Correct composition of dephased behavioural models. Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14. Vol. 10487 Springer, 2017.

Bibtex

@inproceedings{f7f2f645d395405fb99179b14a816895,
title = "Correct composition of dephased behavioural models",
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.",
author = "Juliana Bowles and Caminati, {Marco B}",
year = "2017",
month = sep,
day = "14",
doi = "10.1007/978-3-319-68034-7_14",
language = "English",
isbn = "9783319680347",
volume = "10487",
booktitle = "Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14",
publisher = "Springer",

}

RIS

TY - GEN

T1 - Correct composition of dephased behavioural models

AU - Bowles, Juliana

AU - Caminati, Marco B

PY - 2017/9/14

Y1 - 2017/9/14

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-68034-7_14

DO - 10.1007/978-3-319-68034-7_14

M3 - Conference contribution/Paper

SN - 9783319680347

SN - 9783319680330

VL - 10487

BT - Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings 14

PB - Springer

ER -