Skip to content

Research at St Andrews

Formal verification of CNL health recommendations

Research output: ResearchConference contribution


Open Access permissions



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
StatePublished - 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. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S. 13 Sep 2017 Eleventh International Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, 8 p.

    Research output: ResearchConference contribution

  2. 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: ResearchConference contribution

  3. Weaving true-concurrent aspects using constraint solvers

    Bowles, J. K. F., Bordbar, B. & Alwanain, M. 3 Feb 2017 2016 16th International Conference on Application of Concurrency to System Design (ACSD). IEEE Computer Society, p. 35-44 10 p. 7842499

    Research output: ResearchConference contribution

  4. A flexible approach for finding optimal paths with minimal conflicts

    Bowles, J. K. F. & Caminati, M. B. 2017 Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings. Duan, Z. & Ong, L. (eds.). Springer, p. 209-225 16 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10610)

    Research output: ResearchConference contribution

  5. A verified algorithm enumerating event structures

    Bowles, J. K. F. & Caminati, M. B. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 239-254 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

    Research output: ResearchConference contribution

ID: 250186679