Title

Modelling and model checking suspendible business processes via statechart diagrams and CSP

Document Type

Journal article

Source Publication

Science of Computer Programming

Publication Date

3-1-2007

Volume

65

Issue

1

First Page

14

Last Page

29

Keywords

Statechart diagrams, history mechanism, object behaviour, process modelling, model checking

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 "abnormal" 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. (c) 2006 Elsevier B.V. All rights reserved.

DOI

10.1016/j.scico.2006.08.007

Print ISSN

01676423

E-ISSN

18727964

Publisher Statement

Copyright © 2006 Elsevier B.V

Access to external full text or publisher's version may require subscription.

Full-text Version

Publisher’s Version

Recommended Citation

Yeung, W. L., Leung, K. R. P. H., Wang, J., & Dong, W. (2007). Modelling and model checking suspendible business processes viastatechart diagrams and CSP. Science of Computer Programming, 65(1), 14-29. doi: 10.1016/j.scico.2006.08.007