Secure System Integration and Reliability Improvement (2010)
June 9, 2010 to June 11, 2010
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SSIRI.2010.28
The pacemaker challenge proposed by Software Quality Research Laboratory is looking for formal methods toproduce precise and reliable systems. Safety critical systems like pacemaker need to guarantee important properties (like deadlock-free, safety, etc.), which concern human lives. Formal methods have been applied in designing safety critical systems with verified desirable properties. In this paper, we propose a formal model of pacemaker, modeling its behaviors and its communication with the external environment, using a real-time formalism. Critical properties, such as deadlock freeness and heart rate limits are then verified using the model checker PAT(Process Analysis Toolkit). This work yields a verified formal model of pacemaker systems, which can serve as specification for real pacemaker implementations.
Pacemaker, PAT, model checking, verification
L. A. Tuan, Q. T. Tho and M. C. Zheng, "Modeling and Verification of Safety Critical Systems: A Case Study on Pacemaker," Secure System Integration and Reliability Improvement(SSIRI), Singapore, Singapore, 2010, pp. 23-32.