Abstract
We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker.
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.
Similar content being viewed by others
References
Property Specification Language Reference Manual v1.1. Accellera (June 2004), http://www.eda.org/vfv/
Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized büchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169–184. Springer, Heidelberg (2005)
Duret-Lutz, A.: LTL translation improvements in Spot. In: Proceedings of the 5th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011). Electronic Workshops in Computing, British Computer Society, Tunis (2011), http://ewic.bcs.org/category/15853
Duret-Lutz, A., Poitrenaud, D.: SPOT: An Extensible Model Checking Library using Transition-based Generalized Büchi Automata. In: Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004), pp. 76–83. IEEE Computer Society Press, Volendam (2004)
Francez, N.: Fairness. Springer (1986)
Fronc, Ł.: Effective marking equivalence checking in systems with dynamic process creation. In: Proceedings of the 14th International Workshop on Verification of Infinite-State Systems (Infinity 2012), Paris. EPTCS (August 2012)
Fronc, Ł., Pommereau, F.: Optimizing the compilation of Petri Nets models. In: Proceedings of the Second International Workshop on Scalable and Usable Model Checking for Petri Net and other Models of Concurrency (SUMO 2011), vol. 726. CEUR (2011)
Fronc, Ł., Pommereau, F.: Building Petri Nets tools around Neco compiler. In: Proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE 2013), Milano, vol. 989. CEUR (June 2013)
Hillah, L., Kindler, E., Kordon, F., Petrucci, L., Trèves, N.: A primer on the Petri Net Markup Language and ISO/IEC 15909-2. In: Proceedings of the 10th International workshop on Practical Use of Colored Petri Nets and the CPN Tools, CPN 2009 (October 2009)
Kordon, F., et al.: Raw Report on the Model Checking Contest at Petri Nets 2012. CoRR abs/1209.2382 (2012)
Pommereau, F.: Algebras of coloured Petri Nets. LAP LAMBERT Academic Publishing (2010)
Pommereau, F.: Quickly prototyping Petri Nets tools with SNAKES. Petri Net Newsletter (October 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Fronc, Ł., Duret-Lutz, A. (2013). LTL Model Checking with Neco. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_33
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)