Advertisement

Adapting Petri Nets Reductions to Promela Specifications

  • C. Pajault
  • J. -F. Pradat-Peyre
  • P. Rousseau
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)

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.

Keywords

Model Check Boolean Expression Model Checker Spin Software Model Check Dine Philosopher 
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

  1. 1.
    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)Google Scholar
  2. 2.
    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)CrossRefzbMATHGoogle Scholar
  3. 3.
    Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  4. 4.
    Emerson, A., Prasad Sistl, A.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–478. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Haddad, S., Pradat-Peyre, J.: Efficient reductions for LTL formulae verification. Technical report, CEDRIC, CNAM, Paris (2004)Google Scholar
  7. 7.
    Evangelista, S., Haddad, S., Pradat-Peyre, J.F.: New coloured reductions for software validation. In: Workshop on Discrete Event Systems (2004)Google Scholar
  8. 8.
    Haddad, S., Pradat-Peyre, J.-F.: New efficient petri nets reductions for parallel programs verification. Parallel Processing Letters 16(1), 101–116 (2006)MathSciNetCrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
  13. 13.
    Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Cohen, E., Lamport, L.: Reduction in TLA. In: International Conference on Concurrency Theory, pp. 317–331 (1998)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Evangelista, S., Haddad, S., Pradat-Peyre, J.: Coloured Petri nets reductions for concurrent software validation. Technical report, CEDRIC, CNAM, Paris (2004)Google Scholar
  19. 19.
    Berthelot, G.: Checking properties of nets using transformations. In: Rozenberg, G. (ed.) Advances in Petri nets. LNCS, vol. 222. Springer, Heidelberg (1985)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • C. Pajault
    • 1
  • J. -F. Pradat-Peyre
    • 1
  • P. Rousseau
    • 2
  1. 1.LIP6Université Pierre et Marie CurieParisFrance
  2. 2.Cedric-CNAMFrance

Personalised recommendations