Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker

Formal Aspects of Computing - 1999
Diego Latella1, István Majzik2, Mieke Massink1
1Consiglio Nazionale delle Ricerche, Area della Ricerca di Pisa, Istituto CNUCE, Italy, , IT
2Technical University of Budapest, Dept. of Measurement and Information Systems, Budapest, Hungary, , HU

Tóm tắt

Abstract. Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.

Từ khóa


Tài liệu tham khảo

Bo, 1999, A junction between state based and behavioural based specifications

Bondavalli A., 1999, Fourth IEEE International High-Assurance Systems Engineering Symposium, 64 0418

Br, 1997, Interpreting UML-statecharts in a modal µ-calculus. Unpublished manuscript

Fo, 1997, Applying the Standard Object Modeling Language

Har, 1987, Statecharts: A visual formalism for complex systems, Science of Computer Programming. Elsevier, 8, 231, 10.1016/0167-6423(87)90035-9

Har, 1996, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology, 5, 293, 10.1145/235321.235322

Hol, 1991, Design and Validation of Computer Protocols

Hol, 1997, The model checker SPIN, IEEE Transactions on Software Engineering, 23, 279, 10.1109/32.588521

Le, 1995, editors, 10.1007/3-540-60218-6

Latella D., 1999, Towards a formal operational semantics of UML statechart diagrams, 331

Mil, 1989, Communication and Concurrency

Mi, 1997, Third Asian Computing Science Conference. Advances in Computing Sience - ASIAN'97, 181

[Rat97a] Rational Software and Microsoft and Hewlett-Packard and Oracle and Sterling Software and MCI Systemhouse and Unisys and ICON Computing and IntelliCorp and i-Logix and IBM and ObjecTime and Platinum Technology and Ptech and Taskon and Reich Technologies and Softeam., 1997, UML Notation Guide, version 1.1

[Rat97b] Rational Software and Microsoft and Hewlett-Packard and Oracle and Sterling Software and MCI Systemhouse and Unisys and ICON Computing and IntelliCorp and i-Logix and IBM and ObjecTime and Platinum Technology and Ptech and Taskon and Reich Technologies and Softeam. UML Semantics, 1997, version 1.1

Rumbaugh J., 1999, The Unified Modeling Language Reference Manual

Wi, 1998, Proceedings of the ICSE98 Workshop on Precise Semantics for Software Modeling techniques

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Thông tin tác giả