Symbolic model checking of UML activity diagrams

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

169 Citaten (Scopus)
1 Downloads (Pure)


Two translations from activity diagrams to the input language of NuSMV, a symbolic model verifier, are presented. Both translations map an activity diagram into a finite state machine and are inspired by existing statechart semantics. The requirements-level translation defines state machines that can be efficiently verified, but are a bit unrealistic since they assume the perfect synchrony hypothesis. The implementation-level translation defines state machines that cannot be verified so efficiently, but that are more realistic since they do not use the perfect synchrony hypothesis. To justify the use of the requirements-level translation, we show that for a large class of activity diagrams and certain properties, both translations are equivalent: regardless of which translation is used, the outcome of model checking is the same. Moreover, for linear stuttering-closed properties, the implementation-level translation is equivalent to a slightly modified version of the requirements-level translation. We use the two translations to model check data integrity constraints for an activity diagram and a set of class diagrams that specify the data manipulated in the activities. Both translations have been implemented in two tools. We discuss our experiences in applying both translations to model check some large example activity diagrams.
Originele taal-2Engels
Pagina's (van-tot)1-38
Aantal pagina's38
TijdschriftACM Transactions on Software Engineering and Methodology
Nummer van het tijdschrift1
StatusGepubliceerd - 2006


Duik in de onderzoeksthema's van 'Symbolic model checking of UML activity diagrams'. Samen vormen ze een unieke vingerafdruk.

Citeer dit