JUCS - Journal of Universal Computer Science 8(7): 674-697, doi: 10.3217/jucs-008-07-0674
A Framework for Semantics of UML Sequence Diagrams in PVS
expand article infoDemissie B. Aredo‡
‡ Department of Informatics, University of Oslo, Oslo, Norway

Corresponding author: Demissie Aredo ( demissie@ifi.uio.no )

© Demissie Aredo.
This article is freely available under the J.UCS Open Content License.
Citation: Aredo DB (2002) A Framework for Semantics of UML Sequence Diagrams in PVS. JUCS - Journal of Universal Computer Science 8(7): 674-697. https://doi.org/10.3217/jucs-008-07-0674
Open Access
Abstract
This paper presents a framework for representing formal semantics of a subset of the Unified Modeling Language (UML) notation in a higher-order logic, more specifically semantics of UML sequence diagrams is encoded into the Prototype Verification System (PVS). The primary objective of our work is to make UML models amenable to rigorous analysis by providing their precise semantics. This approach paves a way for formal development of systems through a systematic transformation of UML models. This work is a part of a long-term vision to explore how the PVS tool set can be used to underpin practical tools for analyzing UML models. It contributes to the ongoing effort to provide mathematical foundation to UML notations, with the aim of clarifying the semantics of the language as well as supporting the development of semantically-based tools.
Keywords
formal semantics, UML, PVS, formal methods, object-orientation