Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System

被引：19

作者：

Alur R. ^{[1
]}

Arney D. ^{[1
]}

Gunter E.L. ^{[2
]}

Lee I. ^{[1
]}

Lee J. ^{[3
]}

Nam W. ^{[1
]}

Pearce F. ^{[3
]}

Van Albert S. ^{[3
]}

Zhou J. ^{[1
]}

机构：

[1] Department of Computer and Information Science, Levine Hall, University of Pennsylvania, Philadelphia, PA, 19104-6389

[2] NJIT-CCS, Computer Science Department GITC 4400, New Jersey Institute of Technology, Newark, NJ, 07102, University Heights

[3] Walter Reed Army Institute of Research, Silver Spring, MD, 20910-7500

来源：

International Journal on Software Tools for Technology Transfer | 2004年 / 5卷 / 4期

关键词：

CARA system; Formal methods; Requirements formalization; Safety-critical systems; Software verification;

D O I：

10.1007/s10009-003-0132-7

中图分类号：

学科分类号：

摘要：

Reliability of medical devices such as the CARA Infusion Pump Control System is of extreme importance given that these devices are being used on patients in critical condition. The Infusion Pump Control System includes embedded processors and accompanying embedded software for monitoring as well as controlling sensors and actuators that allow the embedded systems to interact with their environments. This nature of the Infusion Pump Control System adds to the complexity of assuring the reliability of the total system. The traditional methods of developing embedded systems are inadequate for such safety-critical devices. In this paper, we study the application of formal methods to the requirements capture and analysis of the Infusion Pump Control System. Our approach consists of two phases. The first phase is to convert the informal design requirements into a set of reference specifications using a formal system, in this case EFSMs (Extended Finite State Machines). The second phase is to translate the reference specifications to the tools supporting formal analysis, such as SCR and Hermes. This allows us to conclude properties of the reference specifications. Our research goal is to develop a framework and methodology for the integrated use of formal methods in the development of embedded medical systems that require high assurance and confidence. © 2004 Springer-Verlag.

引用

页码：308 / 319

页数：11

共 14 条

[1] Alur R., Grosu R., Modular refinement of hierarchic reactive machines, Proceedings of the 27th ACM symposium on principles of programming languages, pp. 390-402, (2000)
[2] Alur R., Grosu R., Hur Y., Kumar V., Lee I., Modular specifications of hybrid systems in Charon, Proceedings of the 3rd international workshop on hybrid systems: Computation and control, pp. 6-19, (2000)
[3] Alur R., Grosu R., McDougall M., Efficient reachability analysis of hierarchical reactive machines, Proceedings of the 12th international conference on computer-aided verification, pp. 280-295, (2000)
[4] Heitmeyer C., Kirby Jr. J., Labaw B., Archer M., Bharadwaj R., Using abstraction and model checking to detect safety violations in requirements specifications, IEEE Trans Softw Eng, 24, 11, pp. 927-948, (1998)
[5] Heitmeyer C.L., Jeffords R.D., Labaw B.G., Automated consistency checking of requirements specifications, ACM Trans Softw Eng Methodol, 5, 3, pp. 231-261, (1996)
[6] Heninger K., Parnas D.L., Shore J.E., Kallander J.W., Software requirements for the a-7e aircraft, (1978)
[7] Heninger K.L., Specifying software requirements for complex systems: new techniques and their application, Softw Eng, 6, 1, pp. 2-13, (1980)
[8] Kirby J., Heitmeyer C., Archer M., Scr: A practical approach to building a high assurance comsec system, Proceedings of the 15th annual computer security applications conference (ACSAC '99), pp. 109-118, (1999)
[9] Mazza C., Fairclough J., Melton B., de Pablo D., Scheffer A., Stevens R., Software engineering standards, (1994)
[10] Miller S.P., Specifying the mode logic of a flight guidance system in CoRE and SCR, Proceedings of the 2nd workshop on formal methods in software practice, pp. 44-53, (1998)

← 1 2 →