Skip to content

Research at St Andrews

Formal verification of CNL health recommendations

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Fahrurrozi Rahman, Juliana Kuster Filipe Bowles

School/Research organisations


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.


Original languageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
EditorsNadia Polikarpova, Steve Schneider
Place of PublicationCham
Number of pages15
ISBN (Electronic)9783319668451
ISBN (Print)9783319668444
Publication statusPublished - 2017
Event13th International Conference on integrated Formal Methods (iFM 2017) - University of Torino, Torino, Italy
Duration: 18 Sep 201722 Sep 2017
Conference number: 13

Publication series

NameLecture Notes in Computer Science (Programming and Software Engineering)
PublisherSpringer International Publishing
ISSN (Electronic)0302-9743


Conference13th International Conference on integrated Formal Methods (iFM 2017)
Abbreviated titleiFM
Internet address

    Research areas

  • Formal verification, Controlled natural language, Timed automata, Health recommendations

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

View graph of relations

Related by author

  1. Our data, our society, our health: a vision for inclusive and transparent health data science in the United Kingdom and beyond

    Ford, E., Boyd, A., K. F. Bowles, J., Havard, A., Aldridge, R., Curcin, V., Greiver, M., Harron, K., Katikireddi, V., Rodgers, S. & Sperrin, M., 25 Mar 2019, In : Learning Health Systems. Early View, 12 p., e10191.

    Research output: Contribution to journalArticle

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

  3. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S., 7 Feb 2018, Eleventh International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society, Vol. 2018-January. p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Annotated BPMN models for optimised healthcare resource planning

    Bowles, J. K. F., Czekster, R. & Webber, T., 2018, Software Technologies: Applications and Foundations: STAF 2018 Collocated Workshops, Toulouse, France, June 25-29, 2018, Revised Selected Papers. Mazzara, M., Iulian, O. & Salaün, G. (eds.). Cham: Springer, p. 146-162 16 p. (Lecture Notes in Computer Science; vol. 11176).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Estimating capacity and resource allocation in healthcare settings using business process modelling and simulation

    Redeker, G., Webber, T., Czekster, R., Quickert, S. & Bowles, J. K. F., 2 Jul 2017, Anais XXXVII Congresso da Sociedade Brasileira de Computação. Sociedade Brasileira de Computação (SBC), p. 1979-1982

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 250186679