Formal verification of CNL health recommendations

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

1 Citation (Scopus)
4 Downloads (Pure)


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 Sept 201722 Sept 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


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


Dive into the research topics of 'Formal verification of CNL health recommendations'. Together they form a unique fingerprint.

Cite this