Title :
Symbolic model checking supporting formal verification of Grid service workflow models specified by UML activity diagrams
Author :
Hlaoui, Yousra Bendaly ; Benayed, Leila Jemni
Author_Institution :
Res. Unit in Technol. of Inf. & Commun. (UTIC), Inst. of Sci. & Tech. of Tunis, Tunis, Tunisia
fDate :
May 31 2010-June 2 2010
Abstract :
Before being executed, Grid workflow activity diagram models should be analyzed and corrected as early as possible to avoid any costly maintenance delays due to runtime errors. To reach this objective, we define a verification framework which verifies UML activity diagrams against some workflow requirements using NuSMV model checker. For this we propose an homomorphic transformation to realize a correct and complete mapping from UML activity diagrams to NuSMV language.
Keywords :
Computer errors; Delay; Encoding; Error correction; Formal verification; Information analysis; Runtime; Unified modeling language; Web services; XML;
Conference_Titel :
New Technologies of Distributed Systems (NOTERE), 2010 10th Annual International Conference on
Conference_Location :
Tozeur, Tunisia
Print_ISBN :
978-1-4244-7067-9
Electronic_ISBN :
978-1-4244-7068-6
DOI :
10.1109/NOTERE.2010.5536654
