Formal verification of CNL health recommendations

Fahrurrozi Rahman; Juliana Kuster Filipe Bowles

doi:10.1007/978-3-319-66845-1_24

Formal verification of CNL health recommendations

Fahrurrozi Rahman, Juliana Kuster Filipe Bowles

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Integrated Formal Methods
Subtitle of host publication	13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
Editors	Nadia Polikarpova, Steve Schneider
Place of Publication	Cham
Publisher	Springer
Pages	357-371
Number of pages	15
ISBN (Electronic)	9783319668451
ISBN (Print)	9783319668444
DOIs	https://doi.org/10.1007/978-3-319-66845-1_24
Publication status	Published - 2017
Event	13th International Conference on integrated Formal Methods (iFM 2017) - University of Torino, Torino, Italy Duration: 18 Sept 2017 → 22 Sept 2017 Conference number: 13 http://ifm2017.di.unito.it/

Publication series

Name	Lecture Notes in Computer Science (Programming and Software Engineering)
Publisher	Springer International Publishing
Volume	10510
ISSN (Electronic)	0302-9743

Conference

Conference	13th International Conference on integrated Formal Methods (iFM 2017)
Abbreviated title	iFM
Country/Territory	Italy
City	Torino
Period	18/09/17 → 22/09/17
Internet address	http://ifm2017.di.unito.it/

Keywords

Formal verification
Controlled natural language
Timed automata
Health recommendations

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-319-66845-1_24

iFM2017-FRJB-final
© 2017, Springer International Publishing AG. This work has been made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at link.springer.com / https://doi.org/10.1007/978-3-319-66845-1_24
Accepted author manuscript, 919 KB

Automated Conflict Resolution: Automated Conflic Resolution in Clinical Pathways
Kuster Filipe Bowles, J. (PI)
EPSRC
1/07/15 → 15/12/18
Project: Standard

Cite this

Rahman, F., & Bowles, J. K. F. (2017). Formal verification of CNL health recommendations. In N. Polikarpova, & S. Schneider (Eds.), Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings (pp. 357-371). (Lecture Notes in Computer Science (Programming and Software Engineering); Vol. 10510). Springer. https://doi.org/10.1007/978-3-319-66845-1_24

Rahman, Fahrurrozi ; Bowles, Juliana Kuster Filipe. / Formal verification of CNL health recommendations. Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. editor / Nadia Polikarpova ; Steve Schneider. Cham : Springer, 2017. pp. 357-371 (Lecture Notes in Computer Science (Programming and Software Engineering)).

@inproceedings{6d4534958bfd4d7cbe6728463ff834ca,

title = "Formal verification of CNL health recommendations",

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.",

keywords = "Formal verification, Controlled natural language, Timed automata, Health recommendations",

author = "Fahrurrozi Rahman and Bowles, {Juliana Kuster Filipe}",

note = "This research is partially supported by EPSRC grant EP/M014290/1.; 13th International Conference on integrated Formal Methods (iFM 2017), iFM ; Conference date: 18-09-2017 Through 22-09-2017",

year = "2017",

doi = "10.1007/978-3-319-66845-1_24",

language = "English",

isbn = "9783319668444",

series = "Lecture Notes in Computer Science (Programming and Software Engineering)",

publisher = "Springer",

pages = "357--371",

editor = "Nadia Polikarpova and Steve Schneider",

booktitle = "Integrated Formal Methods",

address = "Netherlands",

url = "http://ifm2017.di.unito.it/",

}

Rahman, F & Bowles, JKF 2017, Formal verification of CNL health recommendations. in N Polikarpova & S Schneider (eds), Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Lecture Notes in Computer Science (Programming and Software Engineering), vol. 10510, Springer, Cham, pp. 357-371, 13th International Conference on integrated Formal Methods (iFM 2017), Torino, Italy, 18/09/17. https://doi.org/10.1007/978-3-319-66845-1_24

Formal verification of CNL health recommendations. / Rahman, Fahrurrozi; Bowles, Juliana Kuster Filipe.
Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. ed. / Nadia Polikarpova; Steve Schneider. Cham: Springer, 2017. p. 357-371 (Lecture Notes in Computer Science (Programming and Software Engineering); Vol. 10510).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Formal verification of CNL health recommendations

AU - Rahman, Fahrurrozi

AU - Bowles, Juliana Kuster Filipe

N1 - Conference code: 13

PY - 2017

Y1 - 2017

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

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

KW - Formal verification

KW - Controlled natural language

KW - Timed automata

KW - Health recommendations

U2 - 10.1007/978-3-319-66845-1_24

DO - 10.1007/978-3-319-66845-1_24

M3 - Conference contribution

SN - 9783319668444

T3 - Lecture Notes in Computer Science (Programming and Software Engineering)

SP - 357

EP - 371

BT - Integrated Formal Methods

A2 - Polikarpova, Nadia

A2 - Schneider, Steve

PB - Springer

CY - Cham

T2 - 13th International Conference on integrated Formal Methods (iFM 2017)

Y2 - 18 September 2017 through 22 September 2017

ER -

Rahman F, Bowles JKF. Formal verification of CNL health recommendations. In Polikarpova N, Schneider S, editors, Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Cham: Springer. 2017. p. 357-371. (Lecture Notes in Computer Science (Programming and Software Engineering)). Epub 2017 Aug 27. doi: 10.1007/978-3-319-66845-1_24

Formal verification of CNL health recommendations

Abstract

Publication series

Conference

Keywords

UN SDGs

Access to Document

Fingerprint

Projects

Automated Conflict Resolution: Automated Conflic Resolution in Clinical Pathways

Cite this