Abstract
Petri nets are widely used in the domain of automated verification through model-checking. In this approach, a Petri Net model of the system of interest is produced and its reachable states are computed, searching for erroneous executions. Model compilation can accelerate this analysis by generating code to explore the reachable states. This avoids the use of a fixed exploration tool involving an “interpretation” of the Petri net structure. In this paper, we show how to compile Petri nets targeting the LLVM language (a high-level assembly language) and formally prove the correctness of the produced code. To this aim, we define a structural operational semantics for the fragment of LLVM we use.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E., Emerson, A., Sifakis, J.: Model checking: Algorithmic verification and debugging. ACM Turing Award (2007)
ADT Coq/INRIA. The Coq proof assistant, http://coq.inria.fr
Evangelista, S.: Méthodes et outils de vérification pour les réseaux de Petri de haut niveau. PhD thesis, CNAM, Paris, France (2006)
Fronc, L.: Analyse efficace des réseaux de Petri par des techniques de compilation. Master’s thesis, MPRI, university of Paris 7 (2010), http://www.ibisc.fr/~lfronc/pub/LF_2010.pdf
Fronc, L., Pommereau, F.: Proving a Petri net model-checker implementation. Technical report, IBISC, University of Évry (2010), http://goo.gl/WMzhp
Fronc, L., Pommereau, F.: Optimizing the compilation of Petri nets models. In: Proc. of SUMo 2011. CEUR, vol. 726 (2011), http://ceur-ws.org/Vol-726
Holzmann, G.J., et al.: Spin, formal verification, http://spinroot.com
Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth-first search. In: Proc. of the 2nd Spin Workshop. AMS (1996)
Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009); ISBN: 978-3-642-00283-0
Lattner, C.: LLVM language reference manual, http://llvm.org/docs/LangRef.html
Lattner, C., et al.: The LLVM compiler infrastructure., http://llvm.org
Lattner, C., et al.: LLVM related publications., http://llvm.org/pubs
Lattner, C., et al.: LLVM users, http://llvm.org/Users.html
Pajault, C., Evangelista, S.: Helena: a high level net analyzer, http://helena.cnam.fr
Paulson, L., Nipkow, T., Wenzel, M.: The Isabelle proof assistant, http://www.cl.cam.ac.uk/research/hvg/Isabelle
Pommereau, F.: Quickly prototyping Petri nets tools with SNAKES. Petri net newsletter (2008)
Reinke, C.: Haskell-coloured Petri nets. In: Koopman, P., Clack, C. (eds.) IFL 1999. LNCS, vol. 1868, pp. 181–198. Springer, Heidelberg (2000)
Xavier Rival. Traces Abstraction in Static Analysis and Program Transformation Abstraction de Traces en Analyse Statique et Transformations de Programmes. PhD thesis, Computer Science Department, École Normale Supérieure (2005)
Verma, K.N., Goubault-Larrecq, J., Prasad, S., Arun-Kumar, S.: Reflecting bDDs in coq. In: Kleinberg, R.D., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 162–181. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fronc, L., Pommereau, F. (2011). Towards a Certified Petri Net Model-Checker. In: Yang, H. (eds) Programming Languages and Systems. APLAS 2011. Lecture Notes in Computer Science, vol 7078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25318-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-25318-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25317-1
Online ISBN: 978-3-642-25318-8
eBook Packages: Computer ScienceComputer Science (R0)