Balancing Prescriptions with Constraint Solvers

  • Juliana K. F. BowlesEmail author
  • Marco B. Caminati
Part of the Computational Biology book series (COBO, volume 30)


Clinical guidelines are evidence-based care plans which detail the essential steps to be followed when caring for patients with a specific clinical problem, usually a chronic disease (e.g. diabetes, cardiovascular disease, chronic kidney disease, cancer, chronic obstructive pulmonary disease, and so on). Recommendations for chronic diseases include the medications (or group of medications) to be given at different stages of the treatment plan. We present an automated approach which combines constraint solvers and theorem provers to find the best solutions for treatment according to different criteria, and avoiding adverse drug reactions as much as possible. We extended the approach here to further refine the choice(s) to avoid dangerous or undesirable side effects.


  1. 1.
    Araújo J, Whittle J, Kim D (2004) Modeling and composing scenario-based requirements with aspects. In: RE 2004. IEEE Computer Society Press, pp 58–67Google Scholar
  2. 2.
    Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. In: Gupta A, Kroening D (eds) Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK)Google Scholar
  3. 3.
    Bjørner N, Phan AD, Fleckenstein L (2015) \(\nu \)z-an optimizing SMT solver. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 194–199CrossRefGoogle Scholar
  4. 4.
    Bowles J (2006) Decomposing interactions. In: Johnson M, Vene V (eds) Algebraic methodology and software technology: 11th international conference, Kuressaare, Estonia, 5–8 July 2006. Lecture notes in computer science, vol 4019. Springer, Berlin, pp 189–203CrossRefGoogle Scholar
  5. 5.
    Bowles J, Bordbar B (2007) A formal model for integrating multiple views. In: ACSD 2007. IEEE Computer Society Press, pp 71–79Google Scholar
  6. 6.
    Bowles J, Caminati M (2016) Mind the gap: addressing behavioural inconsistencies with formal methods. In: 23rd Asia-Pacific software engineering conference (APSEC). IEEE Computer Society, pp 313–320Google Scholar
  7. 7.
    Bowles J, Caminati M (2017) Correct composition of dephased behavioural models. In: Proença J, Lumpe M (eds) Formal aspects of component software (FACS 2017). Lecture notes in computer science, vol 10487. Springer, Berlin, pp 233–250CrossRefGoogle Scholar
  8. 8.
    Bowles J, Caminati M (2017) A flexible approach for finding optimal paths with minimal conflicts. In: International conference on formal engineering methods. Lecture notes in computer science, vol 10610. Springer, Berlin, pp 209–225CrossRefGoogle Scholar
  9. 9.
    Bowles J, Caminati M (2017) A verified algorithm enumerating event structures. In: Geuvers H, England M, Hasan O, Rabe F, Teschke O (eds) Intelligent computer mathematics (CICM 2017). Lecture notes in computer science, vol 10383. Springer, Berlin, pp 239–254Google Scholar
  10. 10.
    Bowles J, Alwanain M, Bordbar B, Chen Y (2015) Matching and merging scenarios automatically with Alloy. In: Hammoudi S et al (eds) Model-driven engineering and software development. Communications in computer and information science, vol 506. Springer, Berlin, pp 100–116Google Scholar
  11. 11.
    Bowles J, Bordbar B, Alwanain M (2015) A logical approach for behavioural composition of scenario-based models. In: Butler M, Conchon S, Zaïdi F (eds) Formal methods and software engineering: 17th international conference on formal engineering methods. Lecture notes in computer science, vol 9407. Springer, Berlin, pp 252–269CrossRefGoogle Scholar
  12. 12.
    Bowles J, Bordbar B, Alwanain M (2016) Weaving true-concurrent aspects using constraint solvers. In: Application of concurrency to system design (ACSD 2016). IEEE Computer Society Press, pp 35–44Google Scholar
  13. 13.
    Bowles J, Caminati MB, Cha S (2017) An integrated framework for verifying multiple care pathways. In: 2017 international symposium on theoretical aspects of software engineering (TASE). IEEE Computer Society Press, pp 1–8Google Scholar
  14. 14.
    Caminati M, Kerber M, Lange C, Rowat C (2015) Sound auction specification and implementation. In: Proceedings of the 16th ACM conference on economics and computation, ACM EC ’15, pp 547–564Google Scholar
  15. 15.
    d’Amore F, Franciosa P, Giaccio R, Talamo M (1997) Maintaining maxima under boundary updates. In: Italian conference on algorithms and complexity. Lecture notes in computer science, vol 1203. Springer, Berlin, pp 100–109Google Scholar
  16. 16.
    Dijkman RM, Dumas M, Ouyang C (2008) Semantics and analysis of business process models in BPMN. Inf Softw Technol 50(12):1281–1294CrossRefGoogle Scholar
  17. 17.
    Hughes L, McMurdo MET, Guthrie B (2013) Guidelines for people not for diseases: the challenges of applying UK clinical guidelines to people with multimorbidity. Age Ageing 42:62–69CrossRefGoogle Scholar
  18. 18.
    Jackson D (2006) Software abstractions: logic, language and analysis. MIT Press, CambridgeGoogle Scholar
  19. 19.
    Klein J, Hélouët L, Jézéquel J (2006) Semantic-based weaving of scenarios. In: AOSD’06. ACM, pp 27–38Google Scholar
  20. 20.
    Kovalov A, Bowles J (2016) Avoiding medication conflicts for patients with multimorbidities. In: 12th international conference on integrated formal methods. Lecture Notes in Computer Science, vol 9681. Springer, Berlin, pp 376–392Google Scholar
  21. 21.
    Küster-Filipe J (2006) Modelling concurrent interactions. Theor Comput Sci 351:203–220MathSciNetCrossRefGoogle Scholar
  22. 22.
    Liang H, Diskin Z, Dingel J, Posse E (2008) A general approach for scenario integration. In: MoDELS 2008. Lecture notes in computer science, vol 5301. Springer, Berlin, pp 204–218Google Scholar
  23. 23.
    Moura LD, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS 2008. Lecture Notes in Computer Science, vol 4963. Springer, Berlin, pp 337–340Google Scholar
  24. 24.
    Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL – a proof assistant for higher-order logic. Lecture notes in computer science, vol 2283. Springer, BerlinGoogle Scholar
  25. 25.
    OMG (2011) Business process model and notation. Version 2.0. OMG., Document ID: formal/2011-01-03
  26. 26.
    OMG (2011) UML: superstructure. Version 2.4.1. OMG., Document ID: formal/2011-08-06
  27. 27.
    Reddy R, Solberg A, France R, Ghosh S (2006) Composing sequence models using tags. In: Proceedings of the MoDELS workshop on aspect oriented modelingGoogle Scholar
  28. 28.
    Reisig W (1985) Petri nets. EATCS monograph, vol 4. Springer, BerlinCrossRefGoogle Scholar
  29. 29.
    Rubin J, Chechik M, Easterbrook S (2008) Declarative approach for model composition. In: MiSE 2008. ACM, pp 7–14Google Scholar
  30. 30.
    Whittle J, Araújo J, Moreira A (2006) Composing aspect models with graph transformations. In: Proceedings of the 2006 international workshop on early aspects at ICSE. ACM, pp 59–65Google Scholar
  31. 31.
    Widl M, Biere A, Brosch P, Egly U, Heule M, Kappel G, Seidl M, Tompits H (2013) Guided merging of sequence diagrams. In: SLE 2012. Lecture notes in computer science, vol 7745. Springer, Berlin, pp 164–183CrossRefGoogle Scholar
  32. 32.
    Winskel G, Nielsen M (1995) Models for concurrency. In: Abramsky S, Gabbay D, Maibaum T (eds) Semantic modelling, vol 4. Handbook of logic in computer science. Oxford Science Publications, Oxford, pp 1–148Google Scholar
  33. 33.
    Zhang D, Li S, Liu X (2009) An approach for model composition and verification. In: NCM 2009. IEEE Computer Society Press, pp 1102–1107Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.School of Computer ScienceUniversity of St AndrewsSt AndrewsUnited Kingdom

Personalised recommendations