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

Wing Lok YEUNG

doi:10.3217/jucs-010-11-1540

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

Wing Lok YEUNG

Department of Computing and Decision Sciences

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

6 Citations (Scopus)

Abstract

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 language	English
Pages (from-to)	1540-1558
Number of pages	19
Journal	Journal of Universal Computer Science
Volume	10
Issue number	11
DOIs	https://doi.org/10.3217/jucs-010-11-1540
Publication status	Published - 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.

Keywords

B Abstract Machine Notation
Communicating Sequential Processes
Formal methods
UML

Access to Document

10.3217/jucs-010-11-1540Licence: CC BY-ND

https://commons.ln.edu.hk/cgi/viewcontent.cgi?article=8202&context=sw_masterLicence: CC BY-ND

Cite this

@article{8755fcdc35f24796b532498616723102,

title = "Checking consistency between UML class and state models based on CSP and B",

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

keywords = "B Abstract Machine Notation, Communicating Sequential Processes, Formal methods, UML",

author = "YEUNG, {Wing Lok}",

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

year = "2004",

month = jan,

day = "1",

doi = "10.3217/jucs-010-11-1540",

language = "English",

volume = "10",

pages = "1540--1558",

journal = "Journal of Universal Computer Science",

issn = "0958-695X",

publisher = "Technische Universitat Graz from Austria",

number = "11",

}

TY - JOUR

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

AU - YEUNG, Wing Lok

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

PY - 2004/1/1

Y1 - 2004/1/1

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

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

KW - B Abstract Machine Notation

KW - Communicating Sequential Processes

KW - Formal methods

KW - UML

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

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

U2 - 10.3217/jucs-010-11-1540

DO - 10.3217/jucs-010-11-1540

M3 - Journal Article (refereed)

SN - 0958-695X

VL - 10

SP - 1540

EP - 1558

JO - Journal of Universal Computer Science

JF - Journal of Universal Computer Science

IS - 11

ER -

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

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this