The refinement check of added dynamic diagrams based on π-calculus

Abstract EN

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.