Verifying Parallel Algorithms and Programs Using Coloured Petri Nets

Abstract. Coloured Petri nets have proved to be a useful formalism for modeling distributed algorithms, i.e., algorithms where nodes communi-cate via message passing. Here we describe an approach for automatic extraction of models of parallel algorithms and programs, i.e., algorithms and programs where processes communicate via shared memory. The models can be verified for correctness, here to prove absence of mutual exclusion violations and to find dead- and live-locks. This makes it possi-ble to verify software using a model-extraction approach using coloured Petri nets, where a formal model is extracted from runnable code. We extract models in a manner so we can also support a model-driven de-velopment approach, where code is generated from a model, enabling a combined approach, supporting extracting a model from an abstract de-scription and generation of correct implementation code. We illustrate our idea by applying the technique to a parallel implementation of ex-plicit state-space exploration. Our approach builds on having a coloured Petri net model correspond-ing to the program and using the model to verify properties. We have already treated generation of code from coloured Petri nets, so in this paper we focus on the translation the other way around. We have an implementation of the translation from code to coloured Petri nets.