Model checking suspendible business processes via statechart diagrams and CSP

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

Research output: Book Chapters | Papers in Conference ProceedingsConference paper (refereed)Researchpeer-review

Abstract

When using 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.
Original languageEnglish
Title of host publicationModelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006
PublisherINSTICC Press
Pages97-107
Number of pages11
Publication statusPublished - 1 Jan 2006

Fingerprint

Model checking
Industry

Bibliographical note

Paper presented at the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS 2006), in Conjunction with ICEIS 2006, 23-24 May 2006, Paphos, Cyprus.
ISBN of the source publication: 9789728865498

Cite this

YEUNG, W. L., LEUNG, R. P. H. . K., WANG, J., & DONG, W. (2006). Model checking suspendible business processes via statechart diagrams and CSP. In Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006 (pp. 97-107). INSTICC Press.
YEUNG, Wing Lok ; LEUNG, R. P. H., Karl ; WANG, Ji ; DONG, Wei. / Model checking suspendible business processes via statechart diagrams and CSP. Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006. INSTICC Press, 2006. pp. 97-107
@inproceedings{7e92323d288a4295935bac01d4e82f24,
title = "Model checking suspendible business processes via statechart diagrams and CSP",
abstract = "When using 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.",
author = "YEUNG, {Wing Lok} and LEUNG, {R. P. H., Karl} and Ji WANG and Wei DONG",
note = "Paper presented at the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS 2006), in Conjunction with ICEIS 2006, 23-24 May 2006, Paphos, Cyprus. ISBN of the source publication: 9789728865498",
year = "2006",
month = "1",
day = "1",
language = "English",
pages = "97--107",
booktitle = "Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006",
publisher = "INSTICC Press",

}

YEUNG, WL, LEUNG, RPHK, WANG, J & DONG, W 2006, Model checking suspendible business processes via statechart diagrams and CSP. in Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006. INSTICC Press, pp. 97-107.

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

Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006. INSTICC Press, 2006. p. 97-107.

Research output: Book Chapters | Papers in Conference ProceedingsConference paper (refereed)Researchpeer-review

TY - GEN

T1 - 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

N1 - Paper presented at the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS 2006), in Conjunction with ICEIS 2006, 23-24 May 2006, Paphos, Cyprus. ISBN of the source publication: 9789728865498

PY - 2006/1/1

Y1 - 2006/1/1

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

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

UR - http://commons.ln.edu.hk/sw_master/7075

M3 - Conference paper (refereed)

SP - 97

EP - 107

BT - Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006

PB - INSTICC Press

ER -

YEUNG WL, LEUNG RPHK, WANG J, DONG W. Model checking suspendible business processes via statechart diagrams and CSP. In Modelling, simulation, verification and validation of enterprise information systems : proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006 ; in conjunction with ICEIS 2006 ; Paphos, Cyprus, May 2006. INSTICC Press. 2006. p. 97-107