DocumentCode
3366969
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
fYear
2010
fDate
May 31 2010-June 2 2010
Firstpage
255
Lastpage
260
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/NOTERE.2010.5536654
Filename
5536654
Link To Document