JUCS - Journal of Universal Computer Science 10(11): 1540-1558, doi: 10.3217/jucs-010-11-1540
Checking Consistency between UML Class and State Models Based on CSP and B
expand article infoW. L. Yeung‡
‡ Dept of Computing and Decision Sciences, Lingnan University, Hong Kong

Corresponding author: W. Yeung ( wlyeung@ln.edu.hk )

© W. Yeung.
This article is freely available under the J.UCS Open Content License.
Citation: Yeung WL (2004) Checking Consistency between UML Class and State Models Based on CSP and B. JUCS - Journal of Universal Computer Science 10(11): 1540-1558. https://doi.org/10.3217/jucs-010-11-1540
Open Access
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
UML, formal methods, Communicating Sequential Processes, B Abstract Machine Notation