Skip to content

Research at St Andrews

Formal verification of CNL health recommendations

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

DOI

Open Access permissions

Open

Author(s)

Fahrurrozi Rahman, Juliana Kuster Filipe Bowles

School/Research organisations

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

Details

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
PublisherSpringer
Pages357-371
Number of pages15
ISBN (Electronic)9783319668451
ISBN (Print)9783319668444
DOIs
StatePublished - 2017
Event13th International Conference on integrated Formal Methods (iFM 2017) - Torino, Italy

Publication series

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

Conference

Conference13th International Conference on integrated Formal Methods (iFM 2017)
Abbreviated titleiFM
CountryItaly
CityTorino
Period18/09/1722/09/17
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. 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

  2. An integrated framework for verifying multiple care pathways

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

    Research output: Chapter in Book/Report/Conference proceedingConference 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: Chapter in Book/Report/Conference proceedingConference 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: Chapter in Book/Report/Conference proceedingConference 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: Chapter in Book/Report/Conference proceedingConference contribution

ID: 250186679