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 is 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.

• 1. 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?
• 2. 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?
• 3. 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?
• 4. 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?
• 5. 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 will be produced targeted at all three relevant sectors – researchers, regulators and manufacturers.

The first – less formal – outcome will be a comparison of the different approaches to the Pacemaker Challenge, to be available as a Dagstuhl publication. To achieve such a comparison, the organizers will prepare a catalogue of criteria according to which the approaches will be compared. This catalogue will be 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. Participants will also be able to suggest extensions to the catalogue.

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.

• Andrew Butterfield (Trinity College Dublin, IE) [dblp]
• Martin Daumer (Trium Analysis Online GmbH, DE) [dblp]
• John S. Fitzgerald (University of Newcastle, GB) [dblp]
• Michaela Huhn (TU Clausthal, DE) [dblp]
• Zhihao Jiang (University of Pennsylvania - Philadelphia, US) [dblp]
• Soeren Kemmann (Fraunhofer IESE - Kaiserslautern, DE) [dblp]
• Günther Klebes (sepp.med - Röttenbach, DE)
• John Komp (University of Minnesota - Minneapolis, US)
• Peter Gorm Larsen (Aarhus University, DK) [dblp]
• Brian Larson (Kansas State University, US) [dblp]
• Mark Lawford (McMaster University - Hamilton, CA) [dblp]
• Zhiming Liu (Birmingham City University, GB) [dblp]
• Dominique Méry (LORIA - Nancy, FR) [dblp]
• Zaur Molotnikov (fortiss GmbH - München, DE) [dblp]
• Pieter J. Mosterman (The MathWorks Inc. - Natick, US) [dblp]
• Marcel Oliveira (Federal University of Rio Grande do Norte, BR) [dblp]
• Christian Prehofer (fortiss GmbH - München, DE) [dblp]
• Florian Prester (sepp.med - Röttenbach, DE) [dblp]
• Francesca Saglietti (Universität Erlangen-Nürnberg, DE) [dblp]
• Bernhard Schätz (fortiss GmbH - München, DE) [dblp]
• Neeraj Kumar Singh (McMaster University - Hamilton, CA) [dblp]
• Markus Völter (Völter Ingenieurbüro - Stuttgart, DE) [dblp]
• Alan Wassyng (McMaster University - Hamilton, CA) [dblp]
• Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]