CMRS: analysis of Multi-set Rewrite Systems

BARRE

Contents

 BARRE

Introduction

CMRS is a tool for algorithmic verification of invariants for Constrained Petri Nets (CPN). These models may abstract protocoles built from processes with unique identifiers, process creation, inter-process communication by rendez-vous, procedure call.

Constrained Petri Nets

Constrained Petri Nets (CPN for short) [May98] is a finite set of rules of the form 

p1,..,pn -> q1,...,qm : A
where pi and qi are places and A is a formula called transition guard over the variables denoting the data of tokens moving from/to the involved places.

Examples of programs modeled using CPN can be found in [BEDJ09, BJS07].

Verification method

CMRS has as input a CPN model and its invariant property. It does inductive invariant checking for each rule. The verification conditions generated for that belong to a logic fragment, called CML (Colored Marking Logic) defined in [BJS07], for which CMRS includes a decision procedure.

Credits

CMRS is written, debugged, maintained and improved by Mihaela Sighireanu with contributions from and Selma Saidi.

Download

You can download the CMRS tool via HTTP.

For installing CMRS you need:

References

BEDJS09
A. Bouajjani, C. Enea, C. Dragoi, Y. Jusrki and M. Sighireanu, A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes LMCS 2009.
BJS07
A. Bouajjani, Y. Jurski and M. Sighireanu, A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes TACAS 2007.
BJS07f
A. Bouajjani, Y. Jurski and M. Sighireanu, Reasoning about Dynamic Networks of Infinite-State Processes with Global Synchronization Research report

BARRE

Last updated: Wed Feb 19 2020