Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Massink M. A formal testing framework for {UML Statechart Diagrams} behaviours: From theory to automatic verification. In: Sixth IEEE International High-Assurance Systems Engineering Symposium (Boca Raton, Florida). Proceedings, pp. 11--22. A.~Jacobs (ed). IEEE Computer Society Press, 2001. ISBN0-7695-1275-5, 2001.
In this paper we propose a formal testing framework for a behavioural subset of UML Statechart Diagrams (UMLSDs). A new formal operational semantics is defined, which uses the same core semantics introduced in previous work of ours but which is better suited for testing theory. The new semantics is proved consistent with our original one and is guaranteed to generate only finite state machines. Proper testing pre-orders and equivalences are defined which allow to equate/distinguish systems on the basis of their interaction with the surrounding environment, abstracting from their internal structure. Finally, we provide a way for effective automatic verification of testing equivalence of our statecharts, based on existing techniques and tools.
Subject UML

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional