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

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

Research output: Journal PublicationsJournal Article (refereed)Researchpeer-review

10 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 languageEnglish
Pages (from-to)14-29
Number of pages16
JournalScience of Computer Programming
Volume65
Issue number1
DOIs
Publication statusPublished - 1 Mar 2007

Fingerprint

Model checking
Industry

Keywords

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

Cite this

YEUNG, Wing Lok ; LEUNG, R. P. H., Karl ; WANG, Ji ; DONG, Wei. / Modelling and model checking suspendible business processes via statechart diagrams and CSP. In: Science of Computer Programming. 2007 ; Vol. 65, No. 1. pp. 14-29.
@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 = "3",
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",
number = "1",

}

Modelling and model checking suspendible business processes via statechart diagrams and CSP. / YEUNG, Wing Lok; LEUNG, R. P. H., Karl; WANG, Ji; DONG, Wei.

In: Science of Computer Programming, Vol. 65, No. 1, 01.03.2007, p. 14-29.

Research output: Journal PublicationsJournal Article (refereed)Researchpeer-review

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://commons.ln.edu.hk/sw_master/179

U2 - 10.1016/j.scico.2006.08.007

DO - 10.1016/j.scico.2006.08.007

M3 - Journal Article (refereed)

VL - 65

SP - 14

EP - 29

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

IS - 1

ER -