Abstract
When modelling object behaviour with UML statechart diagrams, the history mechanism can be useful for modelling the suspension of a "normal" business process upon certain äbnormal" events together with the subsequent resumption, as illustrated by the examples in this paper. However, previous approaches to model checking statechart diagrams often ignore the history mechanism. We enhanced such a previous approach based on Communicating Sequential Processes (CSP) and developed a support tool for it.
Users
Please
log in to take part in the discussion (add own reviews or comments).