Pacemaker in VDM

The Pacemaker Challenge problem has been proposed by the North American Software Certification Consortium, based on a pacemaker specification offered by Boston Scientific. Participants in the challenge are invited to develop models, designs and implementations, as well as generating evidence that would be of value in certifying the software.

Responses to the challenge have been offered in both Z and VDM. This page is primarily about the VDM response, but see John Fitzgerald's September 2008 presentation for an overview of both models and future development directions.

Latest Status

Hugo Macedo's MSc dissertation illustrated a staged process for the development of a model of the pacemaker controller as a distributed real-time system, validated by testing. For a summary of the approach and initial results, see the paper by Hugo, John and Peter in FM 2008. An experimental user interface for the models has been developed and trialled by Emma, as described in her MSc dissertation.

Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald, Incremental Development of a Distributed Real-Time Model of A Cardiac Pacing System using VDM, in Jorge Cuellar and Tom Maibaum (Eds.), FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Lecture Notes in Computer Science Vol. 5014, ISBN: 9783540682356, May 2008 (Earlier Newcastle Technical Report Version).

Participants

EmmaNicholls, HugoMacedo, JohnFitzgerald, PeterGormLarsen.

Outcomes

• VDM-SL and VDM++ models

• GUI interface.

External resources

The website hosting the public domain system specification is http://www.cas.mcmaster.ca/sqrl/pacemaker.htm

-- JohnFitzgerald - 17 Sep 2008