Model checking is a widely used technique to prove properties such as liveness, deadlock or safety for a given model. Here we introduce model checking of reconfigurable Petri nets. These are Petri nets with a set of rules for changing the net dynamically. We obtain model checking by converting reconfigurable Petri nets to specific Maude modules and using then the LTLR model checker of Maude. The main result of this paper is the correctness of this conversion. We show that the corresponding labelled transitions systems are bisimular. In an ongoing example reconfigurable Petri nets are used to model and to verify partial dynamic reconfiguration of field programmable gate arrays.
CITATION STYLE
Padberg, J., & Schulz, A. (2016). Model checking reconfigurable petri nets with maude. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9761, pp. 54–70). Springer Verlag. https://doi.org/10.1007/978-3-319-40530-8_4
Mendeley helps you to discover research relevant for your work.