Abstract
Intelligent Transport Systems (ITS) tend to be more distributed and embedded. In many cases, continuous physical parameters are part of the systems description. Analysis techniques based on discrete models must integrate such constraints. In this paper, we propose a methodological way to handle such hybrid systems with model checking on Petri Nets and algebraic methods. Our methodology is based on transformations from Coloured Petri Nets (CPN) for their expressiveness to Symmetric Petri Nets (SN) to take advantage of their efficient verification techniques. Our methodology also addresses the impact of discretization on the precision of verification. In scientific computing, the discretization process introduces “error intervals” that could turn a given verified property into a false positive one. In that case, the property to be verified might have to be transformed to cope with such precision errors.
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
Abrial, J.-R.: The B book - Assigning Programs to meanings. Cambridge Univ. Press, Cambridge (1996)
Berthelot, G.: Transformations and decompositions of nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 254, pp. 359–376. Springer, Heidelberg (1987)
Billington, J., Gallasch, G.E., Petrucci, L.: Verification of the class of stop-and-wait protocols modelled by coloured Petri nets. Nord. J. Comput. 12(3), 251–274 (2005)
Bonnefoi, F., Bellotti, F., Scendzielorz, T., Visintainer, F.: SAFESPOT Applications for Infrasructure-based Co-operative Road Safety. In: 14th World Congress and Exhibition on Intelligent Transport Systems and Services (2007)
Bonnefoi, F., Hillah, L., Kordon, F., Renault, X.: Design, modeling and analysis of ITS using UML and Petri Nets. In: 10th International IEEE Conference on Intelligent Transportation Systems (ITSC 2007), pp. 314–319. IEEE Press, Los Alamitos (2007)
Brgan, R., Poitrenaud, D.: An efficient algorithm for the computation of stubborn sets of well formed Petri nets. In: DeMichelis, G., Díaz, M. (eds.) ICATPN 1995. LNCS, vol. 935, pp. 121–140. Springer, Heidelberg (1995)
Brignolo, R.: Co-operative road safety - the SAFESPOT integrated project. In: APSN - APROSYS Conference. Advanced Passive Safety Network (May 2006)
Buchs, D., Guelfi, N.: A formal specification framework for object-oriented distributed systems. IEEE Trans. Software Eng. 26(7), 635–652 (2000)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Covault, R.B.C., Driscoll, D.: Uncertainties and Error Propagation - Appendix V of Physics Lab Manual. Case Western Reserve University (2005)
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed colored nets and symmetric modeling applications. IEEE Trans. Computers 42(11), 1343–1360 (1993)
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A symbolic reachability graph for coloured Petri nets. Theoretical Computer Science 176(1–2), 39–65 (1997)
Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets Performance Evaluation. Special issue on Performance Modeling Tools 24(1&2), 47–68 (1995)
Christofides, P., El-Farra, N.: Control Nonlinear and Hybrid Process Systems: Designs for Uncertainty, Constraints and Time-delays. Springer, Heidelberg (2005)
Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data decision diagrams for Petri net analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 101–120. Springer, Heidelberg (2002)
Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical Decision Diagrams to Exploit Model Structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443–457. Springer, Heidelberg (2005)
The CPN Tools Homepage (2007), http://www.daimi.au.dk/CPNtools
Daniel, J., Luca, D.: IEEE 802.11p: Towards an International Standard for Wireless Access in Vehicular Environments. In: Proceedings of Vehicular Technology Conference, VTC Spring, pp. 2036–2040. IEEE, Los Alamitos (2008)
David, R., Alla, H.: On Hybrid Petri Nets. Discrete Event Dynamic Systems: Theory and Applications 11(1-2), 9–40 (2001)
Dougherty, J., Kohavi, R., Sahami, M.: Supervised and unsupervised discretization of continuous features. In: Int. Conf. on Machine Learning, pp. 194–202 (1995)
Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1–24 (1985)
Frame Forum. The FRAME forum home page, http://www.frame-online.net
Haddad, S.: A reduction theory for coloured nets. In: Rozenberg, G. (ed.) APN 1989. LNCS, vol. 424, pp. 209–235. Springer, Heidelberg (1990)
Haddad, S., Kordon, F., Petrucci, L., Pradat-Peyre, J.-F., Trèves, N.: Efficient State-Based Analysis by Introducing Bags in Petri Net Color Domains. In: 28th American Control Conference (ACC 2009), St-Louis, USA. IEEE, Los Alamitos (2009)
Haddad, S., Pradat-Peyre, J.-F.: New efficient Petri nets reductions for parallel programs verification. Parallel Processing Letters 16(1), 101–116 (2006)
Hamez, A., Kordon, F., Thierry-Mieg, Y., Legond-Aubry, F.: dmcG: a distributed symbolic model checker based on GreatSPN. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 495–504. Springer, Heidelberg (2007)
Hillah, L., Kordon, F., Petrucci, L., Trèves, N.: PN standardisation: A survey. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 307–322. Springer, Heidelberg (2006)
Hugues, J., Thierry-Mieg, Y., Kordon, F., Pautet, L., Baarir, S., Vergnaud, T.: On the Formal Verification of Middleware Behavioral Properties. In: FMICS 2004, pp. 139–157. Elsevier, Amsterdam (2004)
ISO/IEC-JTC1/SC7/WG19. International Standard ISO/IEC 15909: Software and Systems Engineering - High-level Petri Nets, Part 1: Concepts, Definitions and Graphical Notation (December 2004)
Jensen, K., Kristensen, L.M.: Coloured Petri Nets, Modelling and Validation of Concurrent Systems. Monograph. Springer, Heidelberg (2008)
Junttila, T.: On the symmetry reduction method for Petri Nets and similar formalisms. PhD thesis, Helsinki University of Technology, Espoo, Finland (2003)
Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.L.: Multi-Valued Decision Diagrams: Theory and Applications. International Journal on Multiple-Valued Logic 4(1-2), 9–62 (1998)
Kordon, F., Linard, A., Paviot-Adet, E.: Optimized Colored Nets Unfolding. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 339–355. Springer, Heidelberg (2006)
Lakos, C., Lewis, G.: Incremental State Space Construction for Coloured Petri Nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 263–282. Springer, Heidelberg (2001)
Lewis, G.: Incremental specification and analysis in the context of coloured Petri nets. PhD thesis, University of Hobart, Tasmania (2002)
Lindberg, V.: Uncertainties and Error Propagation - Part I of a manual on Uncertainties, Graphing, and the Vernier Caliper. Rochester Inst. of Technology (2000)
LIP6/MoVe. The CPN-AMI home page, http://www.lip6.fr/cpn-ami/
IEEE 802.11 Working Group for WLAN Standards. IEEE 802.11 tm Wireless Local Area Networks. IEEE, Los Alamitos (2008)
ISO TC204 WG-16. CALM architecture. ISO (2007)
Petri Nets Steering Committee. Petri Nets Tool Database: quick and up-to-date overview of existing tools for Petri Nets, http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/db.html
Thierry-Mieg, Y., Dutheillet, C., Mounier, I.: Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 82–101. Springer, Heidelberg (2003)
Varpaaniemi, K., Halme, J., Hiekkanen, K., Pyssysalo, T.: Prod reference manual. Technical report, Helsinki University of Technology (1995)
Vautherin, J.: Parallel systems specifications with coloured Petri nets and algebraic specifications. In: Rozenberg, G. (ed.) APN 1987. LNCS, vol. 266, pp. 293–308. Springer, Heidelberg (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bonnefoi, F., Choppy, C., Kordon, F. (2009). A Discretization Method from Coloured to Symmetric Nets: Application to an Industrial Example. In: Jensen, K., Billington, J., Koutny, M. (eds) Transactions on Petri Nets and Other Models of Concurrency III. Lecture Notes in Computer Science, vol 5800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04856-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-04856-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04854-8
Online ISBN: 978-3-642-04856-2
eBook Packages: Computer ScienceComputer Science (R0)