Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker |
| |
Authors: | Diego Latella Istvan Majzik Mieke Massink |
| |
Affiliation: | (1) Consiglio Nazionale delle Ricerche, Area della Ricerca di Pisa, Istituto CNUCE, Italy, IT;(2) Technical University of Budapest, Dept. of Measurement and Information Systems, Budapest, Hungary, HU |
| |
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.
Received September 1999 / Accepted in revised form February 2000 |
| |
Keywords: | : UML Statechart Diagrams Model-checking Program transformation PROMELA SPIN |
本文献已被 SpringerLink 等数据库收录! |
|