02. – 07. Februar 2014, Dagstuhl-Seminar 14062

The Pacemaker Challenge: Developing Certifiable Medical Devices


Dominique Méry (LORIA – Nancy, FR)
Bernhard Schätz (fortiss GmbH – München, DE)
Alan Wassyng (McMaster University – Hamilton, CA)


Daniel Ratiu (fortiss GmbH – München, DE)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 4, Issue 2 Dagstuhl Report


Pacemakers are typical examples of those medical devices, like insulin pumps, that help save lives when they operate correctly and safely, but may cause grievous harm when they fail. State-of-the art safety standards like IEC 61508 highly recommend (semi-)formal methods for the specification, design, and development of those devices. The Pacemaker Formal Methods Challenge, the first challenge issued by the North American Software Certification Consortium, is hosted by the Software Quality Research Lab at McMaster University, Canada. The challenge is based on a pacemaker specification offered by Boston Scientific, and is part of the verification Grand Challenges which is an international, long-term research programme that seeks to create a substantial and useful body of code that has been verified to the highest standards of rigour and accuracy. The Pacemaker case-study attracted substantial participation during different events in the research community such as workshops at FM2008, FM2009, FHIES 2011, FHIES 2012 and the student competition at ICSE2009 (SCORE). Currently there are more than 10 world-class research institutes and universities that take part in the challenge, and are using different approaches. Today, there is a wide range of approaches in the formal methods community to specify and develop high integrity systems. Many of these formal approaches do not work well on industrial level applications, and so the state of the practice is remarkably deficient, even in the case of systems that require certification according to the highest safety levels. The purpose of this five days seminar was to bring together researchers, regulators, as well as practitioners in the medical field to discuss and compare different approaches for the development of certifiable medical software, and further the state of practice. Listed below are research topics related to development of medical software to be covered in the seminar:

  • Certification: How can formal methods help in the process of certification of embedded medical software? What standards are in current use and in what measure do they cover model based development? How do we address safety, security and privacy now that these implantable devices are equipped with Wi-Fi, Bluetooth and other wireless networking technologies? How do unspecified environmental assumptions affect the final product?
  • Model-based Development: How can established methods for model based development help the building of implantable medical devices? What kind of models (e.g. controlled biological process, hardware platform, safety function) are needed for designing and certifying safety critical medical systems?
  • Medical-domain specific aspects: What are the most important specific non-functional aspects that need to be considered while developing implantable medical devices? How can biological and medical aspects be integrated in the development process?
  • Tooling: What is the current state of the art and practice concerning tools for formal specification that would be useful in the medical device domain?
  • Pragmatics: What is the fitness of different methods for transfer into practice? What do we need to do to ensure that the regulators and workforce are adequately informed of methods and tools that are useful/indispensable in this domain?

As major results of this Dagstuhl Seminar, two publications are targeted at all three relevant sectors researchers, regulators and manufacturers.

The first outcome is a comparison of the different approaches to the Pacemaker Challenge, to be available as a Dagstuhl publication. To achieve such a comparison, the organizers have prepared a catalogue of criteria according to which the approaches are compared. This catalogue was available in advance of the seminar, so presenters can provide a rationale for their classification according to the catalogue, and participants can discuss those classifications.

As a further, more formal result, a joint publication most preferably in the form of a book on the use of rigorous methods for the development of software-intensive medical devices with the pacemaker as a common example will be produced, with the organizers and editors, and all invited research groups as co-authors. Commitment to the participation in this publication will be made a prerequisite for participation in the seminar for members of the research groups having participated in the challenge.

Summary text license
  Creative Commons BY 3.0 Unported license
  Dominique Méry, Bernhard Schätz, and Alan Wassyng


  • Modelling / Simulation
  • Semantics / Formal Methods
  • Software Engineering


  • Embedded systems
  • Real-time systems
  • Medical devices
  • Model-driven development
  • Software certification
  • Validation & verification
  • Formal methods


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.