Boston Scientific has released into the public domain the system specification for a previous generation pacemaker. A major reason for publishing this specification is to have it serve as the basis for a challenge to the formal methods community, in the spirit of other Grand Challenges.

SQRL is delighted to host the PACEMAKER Formal Methods Challenge on this site, and to act as the "manager" of the Challenge. We are also pleased to acknowledge the association of this Challenge with other Grand Challenges.

This Challenge has multiple dimensions/levels. Participants may choose to submit a complete version of the pacemaker software, designed to run on specified PIC hardware - or may choose to submit just a formal requirements documents - or anything in-between.

We also intend to put in place a certification framework to simulate the concept of licensing. This will enable the Challenge "community" to explore the concept of licensing evidence and the role of standards in the production of such software. Furthermore, it will provide a more objective basis for comparison between putative solutions to the Challenge.

We will be populating the site with information and tools that may be useful in addressing the Challenge.

We intend to organize workshops where issues prompted by the Challenge and the proposed solutions can be discussed. We are also intending to publish results of the Challenge after the deadline for submitting solutions.

The "rules" for the Challenge are currently being formulated. A draft of the rules will be made available for comment/suggestions, and will then be finalized, taking into account submitted comments and suggestions.