Skip to content

Research at St Andrews

A framework for automated conflict detection and resolution in medical guidelines

Research output: Contribution to journalArticle


School/Research organisations


Common chronic conditions are routinely treated following standardised procedures known as clinical guidelines. For patients suffering from two or more chronic conditions, known as multimorbidity, several guidelines have to be applied simultaneously, which may lead to severe adverse effects when the combined recommendations and prescribed medications are inconsistent or incomplete. This paper presents an automated formal framework to detect, highlight and resolve conflicts in the treatments used for patients with multimorbidities focusing on medications. The presented extended framework has a front-end which takes guidelines captured in a standard modelling language and returns the visualisation of the detected conflicts as well as suggested alternative treatments. Internally, the guidelines are transformed into formal models capturing the possible unfoldings of the guidelines. The back-end takes the formal models associated with multiple guidelines and checks their correctness with a theorem prover, and inherent inconsistencies with a constraint solver. Key to our approach is the use of an optimising constraint solver which enables us to search for the best solution that resolves/minimises conflicts according to medication efficacy and the degree of severity in case of harmful combinations, also taking into account their temporal overlapping. The approach is illustrated throughout with a real medical example.


Original languageEnglish
Pages (from-to)42-63
Number of pages22
JournalScience of Computer Programming
Early online date10 Jul 2019
Publication statusPublished - 1 Aug 2019

    Research areas

  • Clinical guidelines, Formal methods, SMT solvers, Theorem provers, Isabelle/HOL

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

View graph of relations

Related by author

  1. Formal reasoning over class models with TOMM

    Mendoza Santana, J. J. & Kuster Filipe Bowles, J., 15 Jul 2019, In : Journal of Object Technology. 18, 2, 20 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

Related by journal

  1. 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: 259673549