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)

10 Citations (Scopus)


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
Issue number1
Publication statusPublished - 1 Mar 2007



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

Cite this