CLC number: TP311.5
On-line Access: 2024-08-27
Received: 2023-10-17
Revision Accepted: 2024-05-08
Crosschecked: 2017-11-29
Cited: 0
Clicked: 6555
Feng Sheng, Liang Dou, Zong-yuan Yang. Mechanized semantics and refinement of UML-Statecharts[J]. Frontiers of Information Technology & Electronic Engineering, 2017, 18(11): 1773-1783.
@article{title="Mechanized semantics and refinement of UML-Statecharts",
author="Feng Sheng, Liang Dou, Zong-yuan Yang",
journal="Frontiers of Information Technology & Electronic Engineering",
volume="18",
number="11",
pages="1773-1783",
year="2017",
publisher="Zhejiang University Press & Springer",
doi="10.1631/FITEE.1601196"
}
%0 Journal Article
%T Mechanized semantics and refinement of UML-Statecharts
%A Feng Sheng
%A Liang Dou
%A Zong-yuan Yang
%J Frontiers of Information Technology & Electronic Engineering
%V 18
%N 11
%P 1773-1783
%@ 2095-9184
%D 2017
%I Zhejiang University Press & Springer
%DOI 10.1631/FITEE.1601196
TY - JOUR
T1 - Mechanized semantics and refinement of UML-Statecharts
A1 - Feng Sheng
A1 - Liang Dou
A1 - Zong-yuan Yang
J0 - Frontiers of Information Technology & Electronic Engineering
VL - 18
IS - 11
SP - 1773
EP - 1783
%@ 2095-9184
Y1 - 2017
PB - Zhejiang University Press & Springer
ER -
DOI - 10.1631/FITEE.1601196
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.
[1]Andronick, J., Chetali, B., Ly, O., 2003. Using Coq to verify Java CardTM 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.
Open peer comments: Debate/Discuss/Question/Opinion
<1>