The Refinement Check of Added Dynamic Diagrams
Based
on p-Calculus
Zhou Xiang1 and Shao Zhiqing2
1Qingdao
University, China
2East China University of Science and Technology,
China
Abstract: As
the semi-formal modeling
tool, UML has semantics defaults which may cause confusions or even mistakes in
refinement of models. p-calculus is a formal
specification based on process algebra, which can give strict semantics
description for system behaviors. We seek to clearly define the semantics of
refinement to a model through p- calculus and thus we are able to
propose a formal verification method of the refinement. Employing this method,
we can improve the efficiency of the consistency verification while decreasing
the mistakes in the refinement process.
Keywords: p-calculus; UML; sequence diagram;
statechart diagram; weak open bisimulation.
Received January 21, 2014; accepted December 22, 2014