Modeling and verification of safety critical systems : a case study on pacemaker

• Main Author: Koo, Sheng Kiat
• Other Authors: School of Computer Engineering
• Format: Final Year Project
• Language: English
• Published: 2014
• Subjects: DRNTU::Engineering::Computer science and engineering::Theory of computation::Mathematical logic and formal languages
• Online Access: http://hdl.handle.net/10356/59202
• Institution: Nanyang Technological University

Medical devices such as cardiac pacemaker must be correctly programmed to save lives. History has shown us that software glitch not only result in monetary lost but also a possible lost in life. Safety critical systems such as the cardiac pacemaker must be verified free from software glitches. Traditional testing methodology fails to identify all possible chances of bugs as such over the last 2 decades research into model checking has been gaining momentum. In 2007, Software Quality Research Laboratory introduced the “Pacemaker Formal Methods Challenge” which is to produce and verify pacemaker models using formal methods.