Abstract: The Unified Modeling Language (UML) is an industry standard for modeling analysis and design. However, the semantics of UML is not precisely defined and the correctness of refinement relations cannot be verified. In this study, we use the theorem proof assistant coq to formalize and mechanize the semantics of UML-Statecharts and the refinement relations between models. Based on the mechanized semantics, the desired properties of both the semantics and the refinement relations can be described and proven as predicates and lemmas. This approach provides a promising way to obtain certified fault-free modeling and refinement.

UML状态图的机械语义和精化研究

[1]Andronick, J., Chetali, B., Ly, O., 2003. Using Coq to verify Java Card^TM applet isolation properties. Proc. Int. Conf. on Theorem Proving in Higher Order Logics, p.335-351.

[2]Börger, E., Cavarra, A., Riccobene, E., 2000. Modeling the dynamics of UML state machines. Proc. Int. Workshop on Abstract State Machines, p.223-241.

[3]Broy, M., Cengarle, M., Rumpe, B., et al., 2007. Towards a System Model for UML: the Structural Data Model. http://rzbl04.biblio.etc.tu-bs.de:8080/docportal/servlets/MCRFileNodeServlet/DocPortal_derivate_00003898/Document_00018887.pdf

[4]Dou, L., Lu, L., Yang, Z., et al., 2013. Towards mechanized semantics of UML sequence diagrams and refinement relation. Proc. 24th IASTED Int. Conf. on Modelling and Simulation, p.262-269.

[5]Gonthier, G., 2007. The four colour theorem: engineering of a formal proof. Proc. 8th Asian Symp. on Computer Mathematics, p.333.

[6]Hallerstede, S., Snook, C., 2011. Refining nodes and edges of state machines. Proc. Int. Conf. on Formal Engineering Methods, p.569-584.

[7]Harel, D., Lachover, H., Naamad, A., et al., 1990. STATEMATE: a working environment for the development of complex reactive systems. IEEE Trans. Softw. Eng., 16(4):403-414.

[8]Jörjens, J., 2005. Secure Systems Development with UML. Springer-Verlag Berlin Heidelberg, Germany.

[9]Klein, C., Prehofer, C., Rumpe, B., 1997. Feature specification and refinement with state transition diagrams. Proc. 4th IEEE Workshop on Feature Interactions in Telecommunications Networks and Distributed Systems, p.284-297.

[10]Lano, K., Clark, D., 2008. Semantics and refinement of behavior state machines. Proc. 10th Int. Conf. on Enterprise Information Systems, p.42-49.

[11]Latella, D., Majzik, I., Massink, M., 1999. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Form. Aspec. Comput., 11(6):637-664.

[12]Leroy, X., 2015. The CompCert C verified compiler: documentation and users manual. Inria, 16(5):563-576.

[13]Liu, S., Liu, Y., Andrö, E., et al., 2013. A formal semantics for complete UML state machines with communications. Proc. Int. Conf. on Integrated Formal Methods, p.331-346.

[14]Prehofer, C., 2013. Behavioral refinement and compatibility of statechart extensions. Electron. Notes Theor. Comput. Sci., 295:65-78.

[15]Said, M., Butler, M., Snook, C., 2009. Language and tool support for class and state machine refinement in UML-B. Proc. Int. Symp. on Formal Methods, p.579-595.

[16]Scholz, P., 2001. Incremental design of statechart specifications. Sci. Comput. Program., 40(1):119-145.

[17]Simons, A., 2000. On the compositional properties of UML statechart diagrams. Proc. Rigorous Object-Oriented Methods Conf., p.1-12.

[18]Snook, C., Butler, M., 2008. UML-B and Event-B: an integration of languages and tools. Proc. IASTED Int. Conf. on Software Engineering, p.336-341.

[19]Sun, M., Zhang, N., Barbosa, L., 2004. On semantics and refinement of UML statecharts: a coalgebraic view. Proc. 2nd Int. Conf. on Software Engineering and Formal Methods, p.164-173.

[20]von der Beeck, M., 2002. A structured operational semantics for UML-statecharts. Softw. Syst. Model., 1(2):130-141.