Abstract
The interleaving of concurrent processes actions leads to the well-known combinatorial explosion problem. Petri nets theory provides some structural reductions to tackle this phenomenon by agglomerating sequences of transitions into a single atomic transition. These reductions are easily checkable and preserve deadlocks, Petri nets liveness and any LTL formula that does not observe the modified transitions. Furthermore, they can be combined with other kinds of reductions such as partial-order techniques to improve the efficiency of state space reduction. We present in this paper an adaptation of these reductions for Promela specifications and propose simple rules to automatically infer atomic steps in the Promela model while preserving the checked property. We demonstrate on typical examples the efficiency of this approach and propose some perspectives of this work in the scope of software model checking.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Wolper, P., Godefroid, P.: Partial-order methods for temporal verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 233–246. Springer, Heidelberg (1993)
Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Form. Methods Syst. Des. 2(2), 149–164 (1993)
Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)
Emerson, A., Prasad Sistl, A.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–478. Springer, Heidelberg (1993)
Sistla, A.P.: Symmetry reductions in model-checking. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575. Springer, Heidelberg (2002)
Haddad, S., Pradat-Peyre, J.: Efficient reductions for LTL formulae verification. Technical report, CEDRIC, CNAM, Paris (2004)
Evangelista, S., Haddad, S., Pradat-Peyre, J.F.: New coloured reductions for software validation. In: Workshop on Discrete Event Systems (2004)
Haddad, S., Pradat-Peyre, J.-F.: New efficient petri nets reductions for parallel programs verification. Parallel Processing Letters 16(1), 101–116 (2006)
Evangelista, S., Kaiser, C., Pradat-Peyre, J.F., Rousseau, P.: Quasar: a new tool for analysing concurrent programs. In: Rosen, J.-P., Strohmeier, A. (eds.) Ada-Europe 2003. LNCS, vol. 2655. Springer, Heidelberg (2003)
Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997)
Pajault, C., Pradat-Peyre, J.: Static reductions for promela specifications. Technical Report 1005, Conservatoire National des Arts et Métiers, laboratoire Cedric, Paris, France (2006)
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Cohen, E., Lamport, L.: Reduction in TLA. In: International Conference on Concurrency Theory, pp. 317–331 (1998)
Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619. Springer, Heidelberg (2003)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp. 338–349. ACM Press, New York (2003)
Flanagan, C., Qadeer, S.: Transactions for software model checking. In: Cook, B., Stoller, S., Visser, W. (eds.) Electronic Notes in Theoretical Computer Science, vol. 89. Elsevier, Amsterdam (2003)
Evangelista, S., Haddad, S., Pradat-Peyre, J.: Coloured Petri nets reductions for concurrent software validation. Technical report, CEDRIC, CNAM, Paris (2004)
Berthelot, G.: Checking properties of nets using transformations. In: Rozenberg, G. (ed.) Advances in Petri nets. LNCS, vol. 222. Springer, Heidelberg (1985)
Poitrenaud, D., Pradat-Peyre, J.: Pre and post-agglomerations for \(\mathit{LTL}\) model checking. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Pajault, C., Pradat-Peyre, J.F., Rousseau, P. (2008). Adapting Petri Nets Reductions to Promela Specifications. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2008. FORTE 2008. Lecture Notes in Computer Science, vol 5048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68855-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-68855-6_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68854-9
Online ISBN: 978-3-540-68855-6
eBook Packages: Computer ScienceComputer Science (R0)