A Rewriting Logic Based Tool for ECATNets Coverability Analysis

Abstract

To analyze the behavior of Petri nets, the reachability graph allows verifying qualitative properties. However, even for small nets, the reachability graph can become infinite if the analyzed Petri net is unbounded. To deal with the state space explosion problem, lazy construction methods to consider only reduced state spaces have been elaborated. For example, the stubborn set reduced reachability graph is usually much smaller than the complete one, but it exhibits all dead states, if any. For unbounded nets, coverability graphs must be used. ECATNets are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high level Petri nets. The most distinctive feature of ECATNets is that their semantics is defined in terms of rewriting logic and its language Maude, allowing us to built models by formal reasoning. In this paper, we propose a rewriting logic based tool that implements an algorithm aiming the construction of coverability graph for ECATNet. Some qualitative properties such as the absence of deadlock can be checked using the constructed coverability graph. The development of this tool is facilitated thanks to the concept of the reflectivity of rewriting logic : the self-interpretation of this logic allows us both the modelling of an ECATNet and acting on it. The tool is illustrated through an example.
Copyright © 2015 Praise Worthy Prize - All rights reserved.