The Cardiac Pacemaker Case Study and its implementation in Safety-Critical Java']Java and Ravenscar Ada

The cardiac pacemaker has emerged as a case study for evaluating the effectiveness of techniques for the verification and design of embedded systems with complex control requirements. This paper reports on the experiences of using this case study to evaluate the concurrency model of two programming language subsets that target safety-critical systems development: Safety-Critical Java (SCJ), a subset of the Real-Time Specification for Java, and Ravenscar Ada, a subset of the real-time support provided by Ada 2005. Our conclusions are that for SCJ, the lack of explicit support for watch-dog timers results in a software architecture where the time at which significant events occur must be saved, and polling must be used to detect their absence. Although this results in a less efficient system, the scheduling implications for the resulting software architecture are clear. In contrast, Ravenscar Ada's support for primitive timing events allow the construction of a highly optimized reactive solution. However, the timing properties of this solution are a little more complex to determine. Furthermore, the Ada solution requires a redundant task in order to prevent the program from terminating prematurely.