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

fYear

2005

fDate

7-10 Aug. 2005

Firstpage

323

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2005. 48th Midwest Symposium on

Print_ISBN

0-7803-9197-7

Type

conf

DOI

10.1109/MWSCAS.2005.1594104

Filename

1594104