A case study : verifying a mutual exclusion protocol with process creation using graph transformation systems
Fernando Luís Dotti, Barbara König, Osmar Marchi dos Santos, Leila Ribeiro · OPUS Publication Server of the University of Stuttgart (University of Stuttgart) · 2004
We verify a mutual exclusion protocol with dynamic process creation based on token passing. The protocol is specified using object-based graph grammars. We introduce the protocol and show how the mutual exclusion property and other properties can be verified using the tool Augur, a verification tool for graph transformation systems based on an approximated unfolding technique.