Checking consistency between UML class and state models based on CSP and B

Wing Lok YEUNG

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

6 Citations (Scopus)


The B Abstract Machine Notation (AMN) and the notation of Communicating Sequential Processes (CSP) have previously been applied to formalise the UML class and state diagrams, respectively. This paper discusses their integrated use in checking the consistency between the two kinds of UML diagrams based on some recent results of research in integrated formal methods. Through a small information system example, the paper illustrates a, clear-cut separation of concerns in employing the two formal methods. Of particular interest is the treatment of recursive calls within a single class of objects.
Original languageEnglish
Pages (from-to)1540-1558
Number of pages19
JournalJournal of Universal Computer Science
Issue number11
Publication statusPublished - 1 Jan 2004

Bibliographical note

Paper presented at the 2nd International Workshop on Verification and Validation of Enterprise Information Systems, 13-Apr-04, Oporto, Portugal.


  • B Abstract Machine Notation
  • Communicating Sequential Processes
  • Formal methods
  • UML


Dive into the research topics of 'Checking consistency between UML class and state models based on CSP and B'. Together they form a unique fingerprint.

Cite this