Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker
Tóm tắt
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
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