JUCS - Journal of Universal Computer Science 6(11): 1088-1108, doi: 10.3217/jucs-006-11-1088
An Outline of PVS Semantics for UML Statecharts
expand article infoIssa Traoré‡
‡ Department of Electrical and Computer Engineering, University of Victoria, Victoria, Canada

Corresponding author: Issa Traoré ( itraore@ece.uvic.ca )

© Issa Traoré.
This article is freely available under the J.UCS Open Content License.
Citation: Traoré I (2000) An Outline of PVS Semantics for UML Statecharts. JUCS - Journal of Universal Computer Science 6(11): 1088-1108. https://doi.org/10.3217/jucs-006-11-1088
Open Access
Abstract
The current UML standard provides definitions for the semantics of its components. These definitions focus mainly on the static structure of UML, but they don t include an execution semantics. These definitions 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 Specification Language as formal semantics domain. We present also how the approach can be used to conduct a formal analysis using the PVS model-checker.
Keywords
open distributed systems, formal methods, object-orientation, UML, PVS, specification