Document Type

Journal article

Source Publication

Journal of Universal Computer Science

Publication Date

1-1-2004

Volume

10

Issue

11

First Page

1540

Last Page

1558

Keywords

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

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.

DOI

10.3217/jucs-010-11-1540

Print ISSN

0958695X

Publisher Statement

Copyright © J.UCS. Access to external full text or publisher's version may require subscription.

Additional Information

Paper presented at the 2nd International Workshop on Verification and Validation of Enterprise Information Systems, 13-Apr-04, Oporto, Portugal. J.UCS is under creative commons "Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)" license starting with issue 1.

Full-text Version

Publisher’s Version

Language

English

Recommended Citation

Yeung, W. L. (2004). Checking consistency between UML class and state models based on CSP and B. Journal of Universal Computer Science, 10(11), 1540-1558. doi: 10.3217/jucs-010-11-1540

Share

COinS