A Flexible Approach for Finding Optimal Paths with Minimal Conflicts | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Flexible Approach for Finding Optimal Paths with Minimal Conflicts

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10610))

Included in the following conference series:

  • 1001 Accesses

Abstract

Complex systems are usually modelled through a combination of structural and behavioural models, where separate behavioural models make it easier to design and understand partial behaviour. When partial models are combined, we need to guarantee that they are consistent, and several automated techniques have been developed to check this. We argue that in some cases it is impossible to guarantee total consistency, and instead we want to find execution paths across such models with minimal conflicts with respect to a certain metric of interest. We present an efficient and scalable solution to find optimal paths through a combination of the theorem prover Isabelle with the constraint solver Z3. Our approach has been inspired by a healthcare problem, namely how to detect conflicts between medications taken by patients with multiple chronic conditions, and how to find preferable alternatives automatically.

This research is supported by EPSRC grant EP/M014290/1.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://pathways.nice.org.uk/.

  2. 2.

    http://www.drugs.com/drug_interactions.html.

  3. 3.

    Cytoscape is a software platform for the visualisation of complex network integrated with any type of attribute data, with a focus on molecular interaction networks. It was chosen among several other visualisation platforms because of the variety of layout algorithms available, the simple data import/export format available, and the relatively moderate adoption effort it required from us.

References

  1. Araújo, J., Whittle, J., Kim, D.: Modeling and composing scenario-based requirements with aspects. In: Proceedings of the 12th IEEE International Requirements Engineering Conference, pp. 58–67. IEEE Computer Society Press (2004)

    Google Scholar 

  2. Bjørner, N., Phan, A.-D., Fleckenstein, L.: vZ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_14

    Google Scholar 

  3. Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53–64 (2011)

    Google Scholar 

  4. Bowles, J.K.F., Bordbar, B., Alwanain, M.: A logical approach for behavioural composition of scenario-based models. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 252–269. Springer, Cham (2015). doi:10.1007/978-3-319-25423-4_16

    Chapter  Google Scholar 

  5. Bowles, J., Bordbar, B.: A formal model for integrating multiple views. In: Seventh International Conference on Application of Concurrency to System Design, 2007, ACSD 2007, pp. 71–79. IEEE Computer Society Press (2007)

    Google Scholar 

  6. Bowles, J., Bordbar, B., Alwanain, M.: Weaving true-concurrent aspects using constraint solvers. In: Application of Concurrency to System Design (ACSD 2016). IEEE Computer Society Press, June 2016

    Google Scholar 

  7. Bowles, J.K.F., Caminati, M.B.: Mind the gap: addressing behavioural inconsistencies with formal methods. In: 2016 23rd Asia-Pacific Software Engineering Conference (APSEC). IEEE Computer Society (2016)

    Google Scholar 

  8. Boyd, C.M., Darer, J., Boult, C., Fried, L.P., Boult, L., Wu, A.W.: Clinical practice guidelines and quality of care for older patients with multiple comorbid diseases: implications for pay for performance. JAMA 294(6), 716–724 (2005)

    Article  Google Scholar 

  9. Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)

    Google Scholar 

  10. Jafarpour, B., Abidi, S.S.R.: Merging disease-specific clinical guidelines to handle comorbidities in a clinical decision support setting. In: Peek, N., Marín Morales, R., Peleg, M. (eds.) AIME 2013. LNCS, vol. 7885, pp. 28–32. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38326-7_5

    Chapter  Google Scholar 

  11. Klein, J., Hélouët, L., Jézéquel, J.: Semantic-based weaving of scenarios. In: Proceedings of the 5th International Conference on Aspect-Oriented Software Development, pp. 27–38. ACM (2006)

    Google Scholar 

  12. Kovalov, A., Bowles, J.K.F.: Avoiding medication conflicts for patients with multimorbidities. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 376–390. Springer, Cham (2016). doi:10.1007/978-3-319-33693-0_24

    Chapter  Google Scholar 

  13. Liang, H., Diskin, Z., Dingel, J., Posse, E.: A general approach for scenario integration. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 204–218. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87875-9_15

    Chapter  Google Scholar 

  14. Lombardi, M., Milano, M., Benini, L.: Robust scheduling of task graphs under execution time uncertainty. IEEE Trans. Comput. 62(1), 98–111 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  15. López-Vallverdú, J.A., Riaño, D., Collado, A.: Rule-based combination of comorbid treatments for chronic diseases applied to hypertension, diabetes mellitus and heart failure. In: Lenz, R., Miksch, S., Peleg, M., Reichert, M., Riaño, D., ten Teije, A. (eds.) KR4HC/ProHealth -2012. LNCS, vol. 7738, pp. 30–41. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36438-9_2

    Chapter  Google Scholar 

  16. Michalowski, M., Wilk, S., Michalowski, W., Lin, D., Farion, K., Mohapatra, S.: Using constraint logic programming to implement iterative actions and numerical measures during mitigation of concurrently applied clinical practice guidelines. In: Peek, N., Marín Morales, R., Peleg, M. (eds.) AIME 2013. LNCS, vol. 7885, pp. 17–22. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38326-7_3

    Chapter  Google Scholar 

  17. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  18. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9

    MATH  Google Scholar 

  19. OMG: Business Process Model and Notation. Version 2.0. OMG (2011). http://www.omg.org, document id: formal/2011-01-03

  20. OMG: UML: Superstructure. Version 2.4.1. OMG (2011). http://www.omg.org, document id: formal/2011-08-06

  21. Piovesan, L., Molino, G., Terenziani, P.: An ontological knowledge and multiple abstraction level decision support system in healthcare. Decision Anal. 1(1), 1 (2014)

    Google Scholar 

  22. Reddy, R., Solberg, A., France, R., Ghosh, S.: Composing sequence models using tags. In: Proceedings of MoDELS Workshop on Aspect Oriented Modeling (2006)

    Google Scholar 

  23. Rubin, J., Chechik, M., Easterbrook, S.: Declarative approach for model composition. In: MiSE 2008, pp. 7–14. ACM (2008)

    Google Scholar 

  24. Shannon, P., Markiel, A., Ozier, O., Baliga, N.S., Wang, J.T., Ramage, D., Amin, N., Schwikowski, B., Ideker, T.: Cytoscape: a software environment for integrated models of biomolecular interaction networks. Genome Res. 13(11), 2498–2504 (2003)

    Article  Google Scholar 

  25. Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng. 35(3), 384–406 (2009)

    Article  Google Scholar 

  26. Whittle, J., Araújo, J., Moreira, A.: Composing aspect models with graph transformations. In: Proceedings of the 2006 International Workshop on Early Aspects at ICSE, pp. 59–65. ACM (2006)

    Google Scholar 

  27. Widl, M., Biere, A., Brosch, P., Egly, U., Heule, M., Kappel, G., Seidl, M., Tompits, H.: Guided merging of sequence diagrams. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol. 7745, pp. 164–183. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36089-3_10

    Chapter  Google Scholar 

  28. Zhang, D., Li, S., Liu, X.: An approach for model composition and verification. In: NCM 2009, pp. 1102–1107. IEEE Computer Society Press (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of St Andrews, St Andrews, KY16 9SX, UK

    Juliana K. F. Bowles & Marco B. Caminati

Authors
  1. Juliana K. F. Bowles
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marco B. Caminati
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Juliana K. F. Bowles .

Editor information

Editors and Affiliations

  1. Xidian University, Xi’an, China

    Zhenhua Duan

  2. University of Oxford, Oxford, United Kingdom

    Luke Ong

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bowles, J.K.F., Caminati, M.B. (2017). A Flexible Approach for Finding Optimal Paths with Minimal Conflicts. In: Duan, Z., Ong, L. (eds) Formal Methods and Software Engineering. ICFEM 2017. Lecture Notes in Computer Science(), vol 10610. Springer, Cham. https://doi.org/10.1007/978-3-319-68690-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68690-5_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68689-9

  • Online ISBN: 978-3-319-68690-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation