A graph transformation-based approach to formal modeling and verification of workflows

Abstract

This paper proposes a formal approach to modeling and verification of workflows using graph transformation systems. To model workflows, we use UML 2.0 activity diagrams. As this kind of diagram does not possess a precise formal semantics, therefore we propose a formal semantics for dynamic behavior of activity diagrams using graph transformation systems and then we verify them by model checking. To verify workflows, we use our previous approach to model checking of graph transformation systems - using Bogor model checker to verify graph transformation systems. © 2008 Springer-Verlag.