An Outline of PVS Semantics for UML Statecharts
Issa Traoré · Zenodo (CERN European Organization for Nuclear Research) · 2020
Abstract: The current UML standard provides de nitions for the semantics of its components. These de nitions focus mainly on the static structure of UML, but they don't include an execution semantics. These de nitions include several "semantic variation points " leaving out the door open for multiple interpretations of the concepts involved. This situation can be handled by formalizing the semantic concepts involved. In this paper we present an approach for the formalization of one of the multiple diagrams of UML, namely statechart diagrams. That is achieved by using the PVS Speci cation Language as formal semantics domain. We present also how the approach can be used to conduct a formal analysis using the PVS model-checker.