RECORD
Formalism for Supporting the Development of Verifiably Safe Medical Guidelines with Statecharts
Software Engineering · Submitted 23 Sep 2019
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. Hence, formal verification is also needed. The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines. The framework allows computer scientists to work together with medical professionals to transform medical best practice guidelines into executable statechart models, Yakindu in particular, so that medical functionalities and properties can be quickly prototyped and validated. Existing formal verification technologies, UPPAAL timed automata in particular, is integrated into the framework to provide formal verification capabilities to verify safety properties. However, some components used/built into the framework, such as the open-source Yakindu statecharts as well as the transformation rules from statecharts to timed automata, do not have built-in semantics. The ambiguity becomes unavoidable unless formal semantics is defined for the framework, which is what the paper is to present.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. | background 1.00 | 0.05 | 0.04 | asserted 1.00 |
| s1 | Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. | background 0.97 | 0.07 | 0.02 | asserted 1.00 |
| s2 | Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. | background 0.58 | 0.07 | 0.04 | asserted 1.00 |
| s3 | Hence, formal verification is also needed. | gap 0.73 | 0.08 | 0.12 | asserted 0.99 |
| s4 | The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines. | contribution 1.00 | 0.91 | 0.42 | asserted 1.00 |
| s5 | The framework allows computer scientists to work together with medical professionals to transform medical best practice guidelines into executable statechart models, Yakindu in particular, so that medical functionalities and properties can be quickly prototyped and validated. | contribution 0.56 | 0.89 | 0.13 | asserted 1.00 |
| s6 | Existing formal verification technologies, UPPAAL timed automata in particular, is integrated into the framework to provide formal verification capabilities to verify safety properties. | method 0.78 | 0.65 | 0.08 | asserted 1.00 |
| s7 | However, some components used/built into the framework, such as the open-source Yakindu statecharts as well as the transformation rules from statecharts to timed automata, do not have built-in semantics. | gap 0.95 | 0.40 | 0.04 | asserted 0.99 |
| s8 | The ambiguity becomes unavoidable unless formal semantics is defined for the framework, which is what the paper is to present. | contribution 0.54 | 0.38 | 0.24 | asserted 0.98 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. Hence, formal verification is also needed. The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines. The framework allows computer scientists to work together with medical professionals to transform medical best practice guidelines into executable statechart models, Yakindu in particular, so that medical functionalities and properties can be quickly prototyped and validated. Existing formal verification technologies, UPPAAL timed automata in particular, is integrated into the framework to provide formal verification capabilities to verify safety properties. However, some components used/built into the framework, such as the open-source Yakindu statecharts as well as the transformation rules from statecharts to timed automata, do not have built-in semantics. The ambiguity becomes unavoidable unless formal semantics is defined for the framework, which is what the paper is to present.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.