Title :
Run-time monitoring and recovery of Harel statecharts using prioritized non-deterministic statechart specifications
Author :
Drusinsky, Doron
Author_Institution :
Time Rover, Inc., Cupertino, CA, USA
Abstract :
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.
Keywords :
Unified Modeling Language; formal specification; object-oriented methods; program compilers; system monitoring; temporal logic; Harel statecharts; Kasas State bounded existance specification pattern; StateRover; code generator; deterministic UML-statecharts; formal requirement specifications; graphical editor; metric temporal logic; prioritized nondeterministic statechart specifications; run-time monitoring; run-time recovery armor-platter; Books; History; Java; Logic; Missiles; Monitoring; Runtime; Specification languages; Standards publication; Unified modeling language;
Conference_Titel :
Circuits and Systems, 2005. 48th Midwest Symposium on
Print_ISBN :
0-7803-9197-7
DOI :
10.1109/MWSCAS.2005.1594104
