Formal semantics for the PACEMAKER system specification

This paper formally expresses the timing behavior of a cardiac pacemaker as defined in the PACEMAKER System Specification as understood by its principal author. The PACEMAKER System Specification was publicly released by Boston Scientific to provide a real-world subject for application of formal methods in response to Jim Woodcock's request at FM2006 for an industrial Grand Challenge problem. PACEMAKER's use for purposes other than formal methods has been surprising in its variety. Most ambitious is the Software Certification Consortium's mock regulatory submission, PACEMAKER Grand Challenge, to show that a product with safety-critical software is in fact safe. McMaster University is designing a second-generation hardware platform to execute formally-verified software during system feature test validation with an electrical heart simulator to show correct behavior. This paper uses first-order predicates, extended with a simple temporal operator, to formally express what the principal author understands to be \"correct\" behavior defined in PACEMAKER.