An Assertional Language for the Verification of Systems Parametric in Several Dimensions (Preliminary Results)

AbstractWe propose a rich assertional language to be used for symbolic verification of systems with several parametric dimensions. Our approach combines notions coming from different fields. We use Colored Petri Nets [16] to describe nets of processes carrying structured data. We combine concepts coming from constraint programming [23] and multiset rewriting [19] to finitely and concisely represent transitions and infinite collection of states of Colored Petri Nets. Finally, we incorporate these concepts in the verification technique based on backward reachability and upward-closed sets of [1,12]. We obtain a procedure that can be used as an automatic support for attacking parameterized verification problems. We apply these ideas to verify safety properties of a parameterized mutual exclusion algorithm. A number of open questions arise from our preliminary experiments, finding an adequate counterpart of our framework in the world of automated deduction being among the more interesting ones