Runtime verification of statechart implementations

TitleRuntime verification of statechart implementations
Publication TypeJournal Article
Year of Publication2005
AuthorsPintér, G., and Majzik, I.
Pagination148 - 172
Date Published2005
ISBN Number0302-9743

Our paper introduces a runtime verification framework for concurrent monitoring of applications specified by UML statecharts. The approach offers a considerable degree of granularity by (i) enabling the modeler to focus on specific key dependability criteria by defining temporal logic formulae over a behavioral model that is available even in early phases of the development and (ii) by supporting the verification of the final implementation against the fully elaborated UML statechart model. The paper presents an extension of the propositional linear temporal logic that fits to the advanced constructs of UML statecharts and an advanced watchdog scheme for concurrent supervision of program execution based on the statechart specification.