Abstract As thesemi-formalmodeling 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 throughp-calculus and thus we are able to propose a formal verification method of the refinement. Employing this method, we can improve the efficiency of theconsistency verification while decreasing the mistakes in the refinement process.

References

[1]Bonf M., Fantuzzi C.,and Secchi C., PatternsforModel-basedAutomation Software DesignandImplementation, Control Engineering Practice, vol. 21,no. 11,pp. 1608- 1619, 2013.

[2]Bouabana-Tebibel T. and Rubin S., Interleaving Semanticsfor UML 2Interactions using PetriNets, Information Sciences, vol. 232, pp. 276-293, 2013.

[3]Cabot J.,Claris R.,and Riera D., the Verificationof UML/OCLClass Diagramsusing Constraint Programming, Journal of Systems and Software, vol. 93,pp. 1-23, 2014.

[4]Chen X. and Li X D., Calculus Based Approach to Modeling Use Case, Journal of Software, vol.19, no.10, pp.2539-2549, 2008.

[5]Elammari M. and Issa Z., Model Driven Architecture to Develop Multi-Agent Systems, available at: http://itgate.info/elammari/mda.pdf, last visited2013.

[6]Heuer A., Stricker V., Budnik C.,Konrad S., Lauenroth K., and Pohl K.,Variability inActivity Diagramsand PetriNets, Science of Computer Programming, vol. 78,no. 12,pp. 2414-2432, 2013.

[7]Lam V. and Padget J., Equivalences of UMLState Chart DiagramsbyStructural CongruenceandOpen Bisimulations, in Proceedings ofIEEE Symposium on Human Centric Computing Languages and Environments, Auckland, pp. 137-144, 2003.

[8]Lam V. and Padget J., sistencyCheckingof Statechart Diagramsof aClass Hierarchy, in Proceedings ofthe19thEuropean Conference on Object-Oriented Programming, Glasgow, pp. 412-427, 2005.

[9]Lam V. and Padget J., Checkingof Sequence DiagramsandStatechart Diagrams using the -calculus, in Proceedings ofthe 5th International Conference on Integrated Formal Methods, Eindhoven, pp. 347-365, 2005.

[10]Lano K. and Kolahdouz-Rahimi S., - basedSpecificationofModel Transformations, Journal of Systems and Software, vol.86,no. 2, pp. 412-436, 2013.

[11]Li Z., Chen H., and Wang B., Symbolic Transition Graphsand the Early Bisimulation Algorithmof -calculus, Science in China Series E: Technological Sciences, vol.29, no.4, pp.361-371, 1999.

[12]Milner R.,Communication and Concurrency, Prentice Hall, 1989.

[13]Milner R.,Joachim ParrowJ., andDavid Walker.,CalculusofMobile Process, Information and Computation, vol.100, no.1, pp.1-40, 1992.

[14]Miyazaki H., Yokogawa T., Amasaki S.,Asada K.,and SatoY.,Synthesis and Refinement Check of Sequence Diagrams, IEICE transactions on Information and Systems, vol. 95, no.9, pp.2193-2201, 2012.

[15]OMG,available at: http://www.omg.org,last visited2013.

[16]Prehofer C., Behavioral Refinement and Compatibility of Statechart Extensions, Electronic Notes in Theoretical Computer Science, vol. 295, pp. 65-78, 2013.

[17]Queralt A.,Artale A.,Calvanese D.,Teniente E., OCL-Lite: FiniteReasoningon UML/OCL Conceptual Schemas, DataandKnowledge Engineering, vol.73, pp. 1-22, 2012.

[18]Rajabi B. and Lee S., Integration between Object Oriented and Coloured Petri Nets Models, TheInternational Arab Journal of Information Technology,vol. 11,no.4,pp. 406- 415,2014.

[19]Victor B.and Molier F., Mobility Workbench-A Tool for the -Calculus, in Proceedings of the 6thInternational Conference on Computer Aided Verification, Stanford, USA, pp.428-440, 1994.

[20]Yao C., Is Going into the Modal Logic, Studies in Philosophy of Science and Techno logy, vol.27, no.3, pp.36-39, 2010.

[21]Zhao Y., Yang Z., and Xie J., -calculus based Assembly Mechanismof UMLState Diagram and Validation ofModel Refinement, in Proceedings ofInternational Conference on Electronic Computer Technology,Macau, pp.604-609, 2009. Zhou Xiangreceived her ME degree in 2000.Currently, sheis a lecturer in Qingdao University and studying towards PhD degree of Computer Science at East China University of Science and Technology. She has been engaged in researchon formal semantics and softwaremodeling. Shao Zhiqingreceived his MS degree in Pure Mathematics from Institute of Software Chinese AcademyofScience and PhD degree in Computer Software from Shanghai Jiao Tong University. Currently, heis a professor in East China University of Science and Technology. His research interests include software verification and network service.