Formal Verification of CNL Health Recommendations

  • Fahrurrozi Rahman
  • Juliana Küster Filipe BowlesEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


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.


Formal verification Controlled natural language Timed automata Health recommendations 


  1. 1.
    Carvalho, G.H.P.D.: NAT2TEST: Generating Test Cases from Natural Language Requirements based on CSP. Ph.D. thesis (2016)Google Scholar
  2. 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. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 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 CrossRefGoogle Scholar
  5. 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 CrossRefGoogle Scholar
  6. 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 2016Google Scholar
  7. 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. 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)CrossRefGoogle Scholar
  9. 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 CrossRefGoogle Scholar
  10. 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 CrossRefGoogle Scholar
  11. 11.
    Polypharmacy Guidance (2nd Edition). Scottish Government Model of Care Polypharmacy Working Group (2015)Google Scholar
  12. 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 CrossRefGoogle Scholar
  13. 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. 14.
    Hoare, C.A.R.: Communicating Sequential Processes. Commun. ACM 21(8), 666–677 (1978). doi: 10.1145/359576.359585 CrossRefzbMATHGoogle Scholar
  15. 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 CrossRefGoogle Scholar
  16. 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). CrossRefGoogle Scholar
  17. 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 CrossRefGoogle Scholar
  18. 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 CrossRefGoogle Scholar
  19. 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)CrossRefGoogle Scholar
  20. 20.
    Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164–190 (2013)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Fahrurrozi Rahman
    • 1
  • Juliana Küster Filipe Bowles
    • 1
    Email author
  1. 1.School of Computer ScienceSt AndrewsUK

Personalised recommendations