Run-time monitoring and recovery of Harel statecharts using prioritized non-deterministic statechart specifications
Doron Drusinsky · 2005
This paper describes the StateRover, a new graphical editor, code generator, run-time monitor, and run-time recovery armor-platter for Harel statecharts augmented with specifications written using prioritized non-deterministic statecharts and metric temporal logic. The StateRover integrates prioritized non-deterministic statechart specifications with deterministic UML-statecharts thereby enabling run-time recovery of deterministic statecharts upon violation of formal requirement specifications. We also compare a Kasas State bounded existance specification pattern written using non-deterministic statecharts with its LTL counterpart.