Skip to content

Research at St Andrews

Correct composition in the presence of behavioural conflicts and dephasing

Research output: Contribution to journalArticle

Open Access Status

  • Embargoed (until 15/10/20)

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

Details

Original languageEnglish
Article number102323
Number of pages22
JournalScience of Computer Programming
Volume185
Early online date15 Oct 2019
DOIs
Publication statusPublished - 1 Jan 2020

    Research areas

  • Formal methods, SMT solver, Theorem provider, Model composition, Optimisation

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

  5. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S., 7 Feb 2018, 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society, p. 1-8 8 p.

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

Related by journal

  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. Introduction to the special issue on automatic program generation for embedded systems

    Hammond, K. & Kelly, P. H. J., 1 Feb 2012, In : Science of Computer Programming. 77, 2, p. 81-82 2 p.

    Research output: Contribution to journalEditorial

ID: 262070904

Top