TLCharts: armor-plating Harel statecharts with temporal logic conditions
Doron Drusinsky, Man‐Tak Shing · 2004
This paper addresses the need for armor-plating Harel Statechart design specifications of real-time systems with safety requirements (which are commonly written in tempo-ral logic) using a new visual specification language named TLCharts. TLCharts combine the visual and intuitive ap-peal of non-deterministic Harel Statecharts with formal specifications written in Linear-time (Metric) Temporal Logic. We demonstrate such armor-plating with a specifi-cation of the safety-critical computer assisted resuscitation algorithm (CARA) software for a casualty intravenous fluid infusion pump. 1