Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

1 2008

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Semantyka operacyjna wybranych diagramów UML

Niewiadomski A., Penczek W. W., Szreter M.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2008

nr 1009

1-64

Praca przedstawia semantykę operacyjną wybranego podzbioru UML w postaci etykietowanego systemu tranzycyjnego. Semantyka jest podstawą opracowywanego weryfikatora modelowego dla UML. Rozważany fragment UML zawiera diagramy klas, diagramy obiektów i diagramy maszyn stanowych. System modelowany za pomocą tych diagramów składa się ze zbioru obiektów oraz zbioru zdarzeń. Statyczna struktura systemu jest definiowana za pomocą diagramu klas i obiektów, podczas gdy zachowanie systemu jest modelowane za pomocą maszyn stanowych. Wykonania zdefiniowanego w pracy systemu tranzycyjnego odpowiadają zachowaniu systemu opisanego za pomocą diagramów UML. Formalnie zdefiniowana semantyka umożliwia przejście do następnego etapu pracy, czyli zakodowania systemu specyfikowanego w UML jako formuły boolowskiej.

The paper presents a semantics of a subset of UML in terms of a labelled transition system. Our further aim is to develop a symbolic model checker for UML based on this semantics. The UML fragment considered consists of class diagrams, object diagrams and state machine diagrams. A system specified in such a subset of UML consists of a set of objects and a set of communication and time events. The static structure of the system is defined by class and object diagrams, whereas its behaviour is determined by state machines. The behaviour of the labelled transition system corresponds to the behaviour of the system specified in UML. A global state consists of an active configuration of each object's statemachine, a valuation of all the variables, a content of event queues and a time component. The transition function defines the state changes corresponding to UML transitions and the time flow. The operational semantics defined as transition system is the starting point to the next stage of the work - a symbolic encoding of the system.