TLCharts: armor-plating Harel statecharts with temporal logic conditions

This paper addresses the need for armor-plating Harel statechart design specifications of real-time systems with safety requirements (which are commonly written in temporal logic) using a new visual specification language named TLCharts. TLCharts combine the visual and intuitive appeal of non-deterministic Harel statecharts with formal specifications written in linear-time (metric) temporal logic. We demonstrate such armor-plating with a specification of the safety-critical computer assisted resuscitation algorithm (CARA) software for a casualty intravenous fluid infusion pump.