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
Publisher
Elsevier BV
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
Funding Information
The first author is supported by Research Grant DR04A7 from Lingnan University. The third author is supported by Program for New Century Excellent Talents in University under Grant No. NCET-04-0996. The third and fourth authors are supported by National Natural Science Foundation of China Grants No. 60233020, 60303013.
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
Language
English
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