On the Similarities of Aircraft and Humans: Monitoring CPS with StreamLAB
Jan Baumeister, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah
Modern medicine increasingly relies on medical cyber-physical systems for diagnosis and treatment of patients. Yet, misbehavior can have dire consequences raising the need for formal guarantees on the runtime behavior. Static verification would provide such guarantees, but is infeasible due to the complexity of the systems and the human physiology. In these cases, more light-weight verification techniques such as runtime monitoring are still applicable. The monitor analyzes a single execution of the system and raises an alarm as soon as it detects unexpected behavior. The shape of unexpected behavior is described in a formal specification language such as the one provided by the StreamLAB framework, which can express complex real-time constraints. Yet the language is sufficiently restrictive to allow for static analyses determining an upper bound on the memory consumption. As a result, the underlying monitoring framework StreamLAB can synthesize an embedded runtime monitor on an FPGA. The practicality of this approach is validated by current case studies on avionics. Moreover, the low memory and energy consumption indicate that a deployment on implantable devices is possible. In this abstract we thus showcase the practicality of StreamLAB in the medical domain and suggest it as a suitable candidate for runtime monitoring on medical devices.