Semantyka operacyjna wybranych diagramów UML

• Autorzy: Niewiadomski A. , Penczek W. W. , Szreter M.

Warianty tytułu

EN

Operational semantics of selected UML diagrams

• Języki publikacji: PL

Abstrakty

PL

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.

EN

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.

Słowa kluczowe

PL

UML; semantyka; czas; weryfikacja modelowa

EN

UML; semantics; time; model checking

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2008
• Tom: nr 1009
• Strony: 1--64
• Opis fizyczny: Bibliogr. 20 poz., rys.

Twórcy

autor

Niewiadomski A.

autor

Penczek W. W.

autor

Szreter M.

• Instytut Informatyki, Akademia Podlaska ul. Sienkiewicza 51 08-110 Siedlce Polska,

Bibliografia

• [1] L. Apvrille, J.-R Courtiat, C. Lohr, P. de Saqui-Sannes (2004) TURTLE: A Real-Time UML Profile Supported by a Formal Validation Toolkit, IEEE Trans. Software Eng, t. 30, nr 7, s. 473-487.
• [2] M. Balser, S. Baumler, A. Knapp, W. Reif, A. Thums (2004) Interactive Verification of UML State Machines, Formal Methods and Software Engineering, s. 434-448.
• [3] G. Behrmann, A. David, K. G. Larsen, J. Hakansson, P. Pettersson, W. Yi, M. Hendriks (2006) UPPAAL 4.0, w: Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST) 2006, IEEE Computer Society, s. 125-126.
• [4] P. Bhaduri, S. Ramesh (2004) Model Checking of Statechart Models: Survey and Research Directions, ArXiv Computer Science e-prints.
• [5] M. Bozga, S. Graf, L Ober, I. Ober, J. Sifakis (2004) The IF Toolset, w: SFM, t. 3185 serii Lecture Notes in Computer Science, s. 237-267, Springer Verlag.
• [6] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella (2002) NuSMY 2: An Open Source Tool for Symbolic Model Checking, w: CAV '02: Proceedings o f the l4th International Conference on Computer Aided Verification, s. 359-364, Springer-Verlag, London, UK, ISBN 3-540-43997-8.
• [7] E. M. Clarke, A. Biere, R. Raimi, Y. Zhu (2001) Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, t. 19, nr l, s. 7-34.
• [8] M. L. Grane, J. Dingel (2005) On the semantics of UML stale machines: Categorization and comparison, Technical Report 2005-501, School of Computing, Queen's University, Kingston, Ontario, Canada.
• [9] W. Damm, B. Josko, A. Pnueli, A. Votintseva (2004) A discrete-time UML semantics for concurrency and communication in safety-critical applications, w: Science of Computer Programming, t. 55, s'. 81-115.
• [10] K. Diethers, U. Goltz, M. Huhn (2002) Model Checking UML Statecharts with Time, w: J. Jürjens, M. V. Cengarle, E. B. Fernandez, B. Rumpe, R. Sandner (red.), Critical Systems Development with UML - Proceedings of the UML'02 workshop, s. 35-52, Technische Universitat München, Institut für Informatik.
• [11] J. Dubrovin, T. Junttila, K. Heljanko (2007) Symbolic step encodings for object based communicating state machines, Technical Report B24, Helsinki University of Technology, Laboratory for Theoretical Computer Science.
• [12] S. Gnesi, D. Latella, M. Massink (2002) Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking, J. Log. Algebr. Program., t. 51, nr l, s. 43-75.
• [13] G. J. Holzmann (2003) The SPIN Model Checker : Primer and Reference Manual, Addison-Wesley Professional.
• [14] A. Janowska, P. Janowski, D. Wróblewski (2007) Translation of Intermediate Language to Timed Automata with Discrete Data, w: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), s. 309-320, Warsaw University.
• [15] T. Jussila, J. Dubrovin, T. Junttila, T. Latvala, I. Porres (2006) Model checking dynamic and hierarchical UML state machines, w: In Proc. Model Development, Validation and Verification, s. 94-110.
• [16] M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny (2007) VerICS 2006 - A Model Checker for Real-Time and Multi-Agent Systems, w: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), s. 345-356, Warsaw University.
• [17] A. Knapp, S. Merz, C. Rauh (2002) Model Checking – Timed UML State Machines and Collaborations, w: FTRTFT, s. 395-416.
• [18] E. Mota, E. Clarke, A. Groce, W. Oliveira, M. F. Ao, J. Kanda (2004) VeriAgent: an Approach to Integrating UML and Formal, ,Eectronic Notes in Theoretical Computer Science, t. 95, s. 111-129.
• [19] A. Niewiadomski, W. Penczek, S. Lasota, J. Kowalski (2006) Weryfikacja UML z wykorzystaniem systemu VerlCS, w: Mat XIII Konferencji Systemy Czasu Rzeczywistego (SCR '06) Systemy informatyczne z ograniczeniami czasowymi, s. 79-91, Wyd. Komunikacji i Łączności.
• [20] OMG (2007) Unified Modeling Language, http://www.omg.org/spec/UML/2.1.2.