An Outline of PVS Semantics for UML Statecharts
Дата
Авторы
Traoré,Issa
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
open distributed systems , formal methods , object-orientation , UML , PVS , specification