Formal Verification of Medical Monitoring Software Using Z Language: A Representative Sample

被引：10

作者：

Babamir, Seyed Morteza ^{[1
]}

Borhani, Mehdi ^{[1
]}

机构：

[1] Univ Kashan, Kashan, Iran

来源：

JOURNAL OF MEDICAL SYSTEMS | 2012年 / 36卷 / 04期

关键词：

Monitoring devices; Insulin pump; Formal language; Verification; DESIGN;

D O I：

10.1007/s10916-011-9739-5

中图分类号：

R19 [保健组织与事业（卫生事业管理）];

学科分类号：

摘要：

Medical monitoring systems are useful aids assisting physicians in keeping patients under constant surveillance; however, taking sound decision by the systems is a physician concern. As a result, verification of the systems behavior in monitoring patients is a matter of significant. The patient monitoring is undertaken by software in modern medical systems; so, software verification of modern medial systems have been noticed. Such verification can be achieved by the Formal Languages having mathematical foundations. Among others, the Z language is a suitable formal language has been used to formal verification of systems. This study aims to present a constructive method to verify a representative sample of a medical system by which the system is visually specified and formally verified against patient constraints stated in Z Language. Exploiting our past experience in formal modeling Continuous Infusion Insulin Pump (CIIP), we think of the CIIP system as a representative sample of medical systems in proposing our present study. The system is responsible for monitoring diabetic's blood sugar.

引用

页码：2633 / 2648

页数：16

共 18 条

[1] FDA: Between Process & Product Evaluation
Abdeen, Marwan M.
Kahl, Wolfram
Maibaum, Tom
[J]. 2007 JOINT WORKSHOP ON HIGH CONFIDENCE MEDICAL DEVICES, SOFTWARE AND SYSTEMS AND MEDICAL DEVICE PLUG-AND PLAY INTEROPERABILITY, 2007, : 181 - 186
[2] Constructing a Model-Based Software Monitor for the Insulin Pump Behavior
Babamir, Seyed Morteza
[J]. JOURNAL OF MEDICAL SYSTEMS, 2012, 36 (02) : 829 - 840
[3] Bagherzadeh Rafsanjani G.H., 1992, P Z US WORKSH
[4] Design and Verification of Systems with Exogenous Coordination Using Vereofy
Baier, Christel
Blechmann, Tobias
Klein, Joachim
Klueppelholz, Sascha
Leister, Wolfgang
[J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 97 - +
[5] Becker U, 2009, LECT NOTES COMPUT SC, V5775, P4, DOI 10.1007/978-3-642-04468-7_2
[6] Capozucca A, 2006, LECT NOTES COMPUT SC, V4157, P59
[7] Conboy HM, 2010, P 1 ACM INT HLTH INF, V1, P656
[8] David R., 2005, DISCRETE CONTINUOUS
[9] A Survey of Software Engineering Techniques in Medical Device Development
Feldmann, Raimund L.
Shull, Forrest
Denger, Christian
Host, Martin
Lindholm, Christin
[J]. 2007 JOINT WORKSHOP ON HIGH CONFIDENCE MEDICAL DEVICES, SOFTWARE AND SYSTEMS AND MEDICAL DEVICE PLUG-AND PLAY INTEROPERABILITY, 2007, : 46 - +
[10] Design Choices for High-Confidence Distributed Real-Time Software
Fischmeister, Sebastian
Azim, Akramul
[J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 327 - 342

← 1 2 →