DocumentCode :
3491662
Title :
Modeling and Model Checking of a Clinical Diagnostic Algorithm
Author :
Ding, Junhua ; Tabrizi, M.N.H.
Author_Institution :
East Carolina Univ., Greenville
fYear :
2008
fDate :
6-8 April 2008
Firstpage :
78
Lastpage :
83
Abstract :
This paper proposes a framework to ensure the correctness of safety critical systems through formally modeling and model checking a clinical diagnostic algorithm. Petri nets are chosen to model the algorithm, and model checker NuSMV is used to verify the properties. The graphic notation of the framework provides a convenient way to facilitate the communication between algorithm designers and software developers. The mathematic foundation of the framework supports precise specification and formal analysis of the algorithm. In addition, the model checking tool provides an automatic approach to guarantees the correctness of the algorithm. The approach in this paper can be easily generalized to accommodate other systems.
Keywords :
Petri nets; formal specification; formal verification; medical diagnostic computing; safety-critical software; NuSMV model checker; Petri nets graphic notation; clinical diagnostic algorithm; formal analysis; formal modeling; formal specification; formal verification; safety critical system; Algorithm design and analysis; Automatic testing; Blood; Computer science; Formal languages; Formal specifications; Graphics; Medical diagnostic imaging; Medical tests; Petri nets;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Networking, Sensing and Control, 2008. ICNSC 2008. IEEE International Conference on
Conference_Location :
Sanya
Print_ISBN :
978-1-4244-1685-1
Electronic_ISBN :
978-1-4244-1686-8
Type :
conf
DOI :
10.1109/ICNSC.2008.4525187
Filename :
4525187
Link To Document :
بازگشت