Skip to content

Research at St Andrews

Correct composition of dephased behavioural models

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.


Original languageEnglish
Title of host publicationFormal aspects of component software
Subtitle of host publication14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings
EditorsJosé Proença, Markus Lumpe
Place of PublicationCham
Number of pages18
ISBN (Electronic)9783319680347
ISBN (Print)9783319680330
Publication statusPublished - 2017
Event14th International Conference on Formal Aspects of Component Software - D. Diogo Museum of Archeology and Arts, Braga, Portugal
Duration: 10 Oct 201713 Oct 2017
Conference number: 14

Publication series

NameLecture notes in computer science (programming and software engineering)
ISSN (Print)0302-9743


Conference14th International Conference on Formal Aspects of Component Software
Abbreviated titleFACS
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. A framework for automated conflict detection and resolution in medical guidelines

    Bowles, J., Caminati, M. B., Cha, S. & Mendoza, J., 1 Aug 2019, In : Science of Computer Programming. 182, p. 42-63 22 p.

    Research output: Contribution to journalArticle

  2. An integrated approach to a combinatorial optimisation problem

    Kuster Filipe Bowles, J. & Caminati, M. B., 2019, Integrated Formal Methods: 15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings. Ahrendt, W. & Tapia Tarifa, S. L. (eds.). LNCS ed. Cham: Springer, p. 284-302 19 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 11918).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Balancing prescriptions with constraint solvers

    Bowles, J. K. F. & Caminati, M. B., 2019, Automated Reasoning for Systems Biology and Medicine. Liò, P. & Zuliani, P. (eds.). Cham: Springer, p. 243-267 25 p. (Computational Biology; vol. 30).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  4. Formalization and Automation of Quality Assurance Processes in Radiation Oncology

    Munbodh, R., Zaveri, H., Caminati, M. & Bowles, J., 31 Jul 2018, In : Medical physics. 45, 6, p. E274-E274 1 p.

    Research output: Contribution to journalAbstract

ID: 250701579