Distributed Verification of Occurrence Graphs: Investigating the Use of Computational Grids

We investigated the benefits and drawbacks of a strategy for verification of occurrence graphs that uses computational grids as infrastructure for distribution. This investigation was performed using a tool set for the Petri net formalism and a computational grid for bag-of-tasks applications. Bag-of- tasks applications are those parallel applications whose tasks are independent. The motivation of this investigation are the solutions provided by grid computing for fundamental problems of distributed systems such as, scalability of resource, computation speed up, reliability and security. We obtained interesting results: we always generate and check larger state spaces and observed that performance improvement depends on the partitioning specification used to generate the distributed state space. Good partitioning specifications reduce the time required to perform the verification. Bad partitioning specs, on the other hand, lead to performance even worst than the centralized tool. However an efficient partitioning is very hard to find.