Verifying parallel algorithms and programs using coloured Petri nets

M. Westergaard

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

3 Citations (Scopus)

Abstract

Coloured Petri nets have proved to be a useful formalism for modeling distributed algorithms, i.e., algorithms where nodes communicate 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 possible 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 development approach, where code is generated from a model, enabling a combined approach, supporting extracting a model from an abstract description and generation of correct implementation code. We illustrate our idea by applying the technique to a parallel implementation of explicit state-space exploration. Our approach builds on having a coloured Petri net model corresponding 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.
Original languageEnglish
Title of host publicationTransactions on Petri Nets and Other Models of Concurrency VI
EditorsK. Jensen, W.M.P. Aalst, van der, M. Ajmone Marsan, G. Franceschinis, J. Kleijn, L.M. Kristensen
Place of PublicationBerlin
PublisherSpringer
Pages146-168
ISBN (Print)978-3-642-35178-5
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
Volume7400
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Verifying parallel algorithms and programs using coloured Petri nets'. Together they form a unique fingerprint.

Cite this