Grade/CPN : semi-automatic support for teaching Petri nets by checking many Petri nets against one specification

M. Westergaard, D. Fahland, C. Stahl

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

Abstract

Grading dozens of Petri net models manually is a tedious and error-prone task. In this paper, we present Grade/CPN, a tool supporting the grading of Colored Petri nets modeled in CPN Tools. The tool is extensible, con¿gurable, and can check static and dynamic properties. It automatically handles tedious tasks like checking that good modeling practise is adhered to, and supports tasks that are di¿cult to automatize, such as checking model legibility. We propose and support the Britney Temporal Logic which can be used to guide the simulator and to check temporal properties. We provide our experiences with using the tool in a course with 100 participants.
Original languageEnglish
Title of host publicationProceedings of the International Workshop on Petri Nets and Software Engineering (PNSE'12, Hamburg, Germany, June 25-26, 2012)
EditorsL. Cabac, M. Duvigneau, D. Moldt
PublisherCEUR-WS.org
Pages32-46
Publication statusPublished - 2012
Event33rd International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, Petri Nets 2012 - Hamburg, Germany
Duration: 25 Jun 201229 Jun 2012

Publication series

NameCEUR Workshop Proceedings
Volume851
ISSN (Print)1613-0073

Conference

Conference33rd International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, Petri Nets 2012
Abbreviated titlePNSE '12
Country/TerritoryGermany
CityHamburg
Period25/06/1229/06/12
OtherWorkshop co-located with the 33rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2012) and the 12th International Conference on Application of Concurrency to System Design (ACSD 2012)

Fingerprint

Dive into the research topics of 'Grade/CPN : semi-automatic support for teaching Petri nets by checking many Petri nets against one specification'. Together they form a unique fingerprint.

Cite this