Verification of Medical Guidelines by Model Checking – A Case Study

2006 ◽  
pp. 219-233 ◽  
Author(s):  
Simon Bäumler ◽  
Michael Balser ◽  
Andriy Dunets ◽  
Wolfgang Reif ◽  
Jonathan Schmitt
Keyword(s):  
Model Checking ◽  
Medical Guidelines

scholarly journals Model Checking Contracts – A Case Study

2007 ◽  
pp. 82-97 ◽  
Author(s):  
Gordon Pace ◽  
Cristian Prisacariu ◽  
Gerardo Schneider
Keyword(s):  
Model Checking

Reliability analysis and safety model checking of Safety-Critical and control Systems: A case study of NPP control system

2022 ◽  
Vol 166 ◽  
pp. 108812
Author(s):  
Vinay Kumar ◽  
Kailash Chandra Mishra ◽  
Pooja Singh ◽  
Aditya Narayan Hati ◽  
Mohan Rao Mamdikar ◽  
...  
Keyword(s):  
Control System ◽  
Model Checking ◽  
Reliability Analysis ◽  
Control Systems ◽  
Safety Critical ◽  
And Control

In Silico Laboratory Experiments using Statistical Model Checking: A new model of the Palytoxin-Induced Pump Channel as Case Study

2020 ◽  
pp. 1-1
Author(s):  
Gabriel Domingo Vilallonga ◽  
Daniel Edgardo Riesco ◽  
Antonio-Carlos Guimaraes Almeida ◽  
Antonio Marcio Rodrigues ◽  
Sergio V. A. Campos
Keyword(s):  
Model Checking ◽  
Statistical Model ◽  
In Silico ◽  
Laboratory Experiments ◽  
Statistical Model Checking ◽  
New Model

A Method for the Formal Verification of Human-interactive Systems

2009 ◽  
Vol 53 (12) ◽  
pp. 764-768 ◽  
Author(s):  
Matthew L Bolton ◽  
Ellen J. Bass
Keyword(s):  
Model Checking ◽  
Human Behavior ◽  
Interactive Systems ◽  
Formal Models ◽  
Operational Environment ◽  
Patient Controlled Analgesia ◽  
Operational Conditions ◽  
Analytic Models ◽  
Human Device

Predicting failures in complex, human-interactive systems is difficult as they may occur under rare operational conditions and may be influenced by many factors including the system mission, the human operator's behavior, device automation, human-device interfaces, and the operational environment. This paper presents a method that integrates task analytic models of human behavior with formal models and model checking in order to formally verify properties of human-interactive systems. This method is illustrated with a case study: the programming of a patient controlled analgesia pump. Two specifications, one of which produces a counterexample, illustrate the analysis and visualization capabilities of the method.

Sign in / Sign up

Export Citation Format

Share Document