The Refinement Check of Added Dynamic Diagrams Based on -Calculus

As the semi-formal modeling tool, UML has semantics defaults which may cause confusions or even mistakes in refinement of models. -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- 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