Figure 1: Statechart for the infusion pump control with embedded formal specification assertions.