The computer-assisted resuscitation algorithm (CARA) is the software component of an automatic infusion pump system being designed by US Armys Walter Reed Institute of Research (WRAIR) to be used in the battlefields of tomorrow. Such medical devices are safety critical, and their use needs to be approved by the US Food and Drug Administration (FDA) – a process on which formal methods can have a great impact. In this special section, six papers on the analysis of CARAs requirements are presented. In the rest of this introduction, we present the framework and summary of results from those papers.