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

Wing Lok YEUNG; R. P. H., Karl LEUNG; Ji WANG; Wei DONG

doi:10.1016/j.scico.2006.08.007

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

Wing Lok YEUNG, R. P. H., Karl LEUNG, Ji WANG, Wei DONG

Department of Computing and Decision Sciences

Research output: Journal Publications › Journal Article (refereed) › peer-review

11 Citations (Scopus)

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.

Original language	English
Pages (from-to)	14-29
Number of pages	16
Journal	Science of Computer Programming
Volume	65
Issue number	1
DOIs	https://doi.org/10.1016/j.scico.2006.08.007
Publication status	Published - 1 Mar 2007

Funding

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. The authors would like to thank the anonymous referees for their helpful comments and suggestions.

Keywords

Statechart diagrams
history mechanism
model checking
object behaviour
process modelling

Access to Document

10.1016/j.scico.2006.08.007

Cite this

@article{92ee6b4e53944283949a99a8a2ac2885,

title = "Modelling and model checking suspendible business processes via statechart diagrams and CSP",

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.",

keywords = "Statechart diagrams, history mechanism, model checking, object behaviour, process modelling",

author = "YEUNG, {Wing Lok} and LEUNG, {R. P. H., Karl} and Ji WANG and Wei DONG",

year = "2007",

month = mar,

day = "1",

doi = "10.1016/j.scico.2006.08.007",

language = "English",

volume = "65",

pages = "14--29",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier B.V.",

number = "1",

}

TY - JOUR

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

AU - YEUNG, Wing Lok

AU - LEUNG, R. P. H., Karl

AU - WANG, Ji

AU - DONG, Wei

PY - 2007/3/1

Y1 - 2007/3/1

N2 - 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.

AB - 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.

KW - Statechart diagrams

KW - history mechanism

KW - model checking

KW - object behaviour

KW - process modelling

UR - http://www.scopus.com/inward/record.url?scp=33846566725&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2006.08.007

DO - 10.1016/j.scico.2006.08.007

M3 - Journal Article (refereed)

SN - 0167-6423

VL - 65

SP - 14

EP - 29

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 1

ER -

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

Abstract

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this