Statechart assertions
From Wikipedia, the free encyclopedia
 |
This article or section may be confusing or unclear for many readers. Please improve the article or discuss this issue on the talk page. This article has been tagged since December 2006. |
Statechart assertions are a formal specification interpretation of Harel statecharts developed by Doron Drusinsky. A statechart assertion is used for runtime verification and automatic test generation of some other, design or model, statechart (the "primary" statechart). Statechart assertions provide a requirements-based view of the primary model. A statechart assertion is code-generated into executable C++ or Java code that resides in the System Under Test (SUT) for verification purposes.
Statechart assertions qualify a scenario as being accepted or rejected using a built in Boolean bSuccess flag and a corresponding isSuccess() method. Hence, a statechart assertion behaves like a logic formula: it accepts or rejects sequences of events (secenarios).
Unlike design and model statecharts, statechart assertions can be non-deterministic. Non-deterministic statechart assertions use an existential semantics to decide whether a certain scenario is rejected, namely, if at least one computation rejects the scenario then so does the entire assertion.
Statechart assertions are often used for non-testing purposes, such as run-time recovery from specification violations.
[edit] References
- Drusinsky, Doron (2006). Modeling and Verification Using UML Statecharts. Elsevier. ISBN 0-7506-7949-2.
