Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2017: Integrated Formal Methods pp 357–371Cite as

Formal Verification of CNL Health Recommendations

  • Conference paper
  • First Online:

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

Abstract

Clinical texts, such as therapy algorithms, are often described in natural language and may include hidden inconsistencies, gaps and potential deadlocks. In this paper, we propose an approach to identify such problems with formal verification. From each sentence in the therapy algorithm we automatically generate a parse tree and derive case frames. From the case frames we construct a state-based representation (in our case a timed automaton) and use a model checker (here UPPAAL) to verify the model. Throughout the paper we use an example of the algorithm for blood glucose lowering therapy in adults with type 2 diabetes to illustrate our approach.

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

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • 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

Learn about institutional subscriptions

Notes

  1. 1.

    More details on NICE available at www.nice.org.uk.

  2. 2.

    Full details are available at https://goo.gl/YDDtQY.

  3. 3.

    https://bitbucket.org/modgrammar/modgrammar.

References

  1. Carvalho, G.H.P.D.: NAT2TEST: Generating Test Cases from Natural Language Requirements based on CSP. Ph.D. thesis (2016)

    Google Scholar 

  2. Townsend, H.: Natural language processing and clinical outcomes: the promise and progress of NLP for improved care. J. AHIMA 84(2), 44–45 (2013)

    Google Scholar 

  3. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

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

  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: 23rd Asia-Pacific Software Engineering Conference (APSEC). IEEE Computer Society (2016)

    Google Scholar 

  8. Demner-Fushman, D., Chapman, W.W., McDonald, C.J.: What can natural language processing do for clinical decision support? J. Biomed. Inform. 42(5), 760–772 (2009)

    Article  Google Scholar 

  9. Shah, N.H., LePendu, P., Bauer-Mehren, A., Ghebremariam, Y.T., Iyer, S.V., Marcus, J., Nead, K.T., Cooke, J.P., Leeper, N.J.: Proton pump inhibitor usage and the risk of myocardial infarction in the general population. PLoSONE 10(6), e0124653 (2015). 10.1371/journal.pone.0124653

    Article  Google Scholar 

  10. LePendu, P., Iyer, S.V., Bauer-Mehren, A., Harpaz, R., Mortensen, J., Podchiyska, T., Ferris, T.A., Shah, N.H.: Pharmacovigilance using clinical notes. Clin. Pharmacol. Ther. 93, 547–555 (2013). 10.1038/clpt.2013.47

    Article  Google Scholar 

  11. Polypharmacy Guidance (2nd Edition). Scottish Government Model of Care Polypharmacy Working Group (2015)

    Google Scholar 

  12. Imler, T.D., Morea, J., Kahi, C., Cardwell, J., Johnson, C.S., Xu, H., Imperiale, T.F.: Multi-center colonoscopy quality measurement utilizing natural language processing. Am. J. Gastroenterol. 110(4), 543–552 (2015). 10.1038/ajg.2015.51

    Article  Google Scholar 

  13. Fillmore, C.J.: The case for case. In: Bach, E., Harms, R.T. (eds.) Universals in Linguistic Theory. Holt, Rinehart and Winston, London (1968)

    Google Scholar 

  14. Hoare, C.A.R.: Communicating Sequential Processes. Commun. ACM 21(8), 666–677 (1978). doi:10.1145/359576.359585

    Article  MATH  Google Scholar 

  15. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_13

    Chapter  Google Scholar 

  16. Carvalho, G., Falcão, D., Barros, F., Sampaio, A., Mota, A., Motta, L., Blackburn, M.: NAT2TEST\(_{SCR}\): test case generation from natural language requirements based on SCR specifications. Sci. Comput. Program. 95(Part3), 275–297 (2014). https://doi.org/10.1016/j.scico.2014.06.007

    Article  Google Scholar 

  17. Carvalho, G., Barros, F., Lapschies, F., Schulze, U., Peleska, J.: Model-based testing from controlled natural language requirements. In: Artho, C., Öveczky, P. (eds.) Formal Techniques for Safety-Critical Systems. CCIS, vol. 419, pp. 19–35. Springer, Cham (2013). doi:10.1007/978-3-319-05416-2_3

    Chapter  Google Scholar 

  18. Silva, B.C.F., Carvalho, G., Sampaio, A.: Test case generation from natural language requirements using CPN simulation. In: Cornélio, M., Roscoe, B. (eds.) SBMF 2015. LNCS, vol. 9526, pp. 178–193. Springer, Cham (2016). doi:10.1007/978-3-319-29473-5_11

    Chapter  Google Scholar 

  19. Diamantopoulos, T., Roth, M., Symeonidis, A., Klein, E.: Software requirements as an application domain for natural language processing. Lang. Resour. Eval. 51(2), 495–524 (2017)

    Article  Google Scholar 

  20. Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164–190 (2013)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Fahrurrozi Rahman & Juliana Küster Filipe Bowles

Authors
  1. Fahrurrozi Rahman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Juliana Küster Filipe Bowles
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Juliana Küster Filipe Bowles .

Editor information

Editors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, Massachusetts, USA

    Nadia Polikarpova

  2. University of Surrey, Guildford, United Kingdom

    Steve Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Rahman, F., Bowles, J.K.F. (2017). Formal Verification of CNL Health Recommendations. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66845-1_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66844-4

  • Online ISBN: 978-3-319-66845-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation