Advertisement

Abstract

We define a safety slice as a subnet of a marked Petri net Σ that approximates Σ’s temporal behavior with respect to a set of interesting places Crit. This safety slice can be used to verify and falsify stutter-invariant linear-time safety properties when Crit is the set of places referred to by the safety property. By construction it is guaranteed that the safety slice’s state space is at most as big as that of the original net. Results on a benchmark set demonstrate effective reductions on several net instances. Therefore safety slicing as a net preprocessing step may achieve an acceleration for model checking stutter-invariant linear-time safety properties.

Keywords

State Space Model Check Transition Sequence Safety Property Input Place 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008); 12, 112–120, 422–425Google Scholar
  2. 2.
    Berthelot, G.: Checking Properties of Nets Using Transformation. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222, pp. 19–40. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  3. 3.
    Brückner, I.: Slicing Integrated Formal Specifications for Verification. PhD thesis. University of Paderborn (March 2008)Google Scholar
  4. 4.
    Chang, C.K., Wang, H.: A slicing algorithm of concurrency modeling based on Petri nets. In: Hwang, K., Jacobs, S.M., Swartzlander, E.E. (eds.) Proc. of the 1986 Int. Conf. on Parallel Processing, pp. 789–792. IEEE Computer Society Press, Washington (1987)Google Scholar
  5. 5.
    Corbett, J.C.: Evaluating Deadlock Detection Methods for Concurrent Software. IEEE Transactions on Software Engineering 22(3), 161–180 (1996)CrossRefGoogle Scholar
  6. 6.
    Lamport, L.: What Good is Temporal Logic? In: Information Processing 1983: Proceedings of the IFIO 9th World Computer Congress, pp. 657–668 (1983)Google Scholar
  7. 7.
    Llorens, M., Oliver, J., Silva, J., Tamarit, S., Vidal, G.: Dynamic Slicing Techniques for Petri Nets. In: Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008), Liverpool, UK. Electronic Notes in Theoretical Computer Science, vol. 223, pp. 153–165 (December 2008)Google Scholar
  8. 8.
    Peled, D., Wilke, T.: Stutter-Invariant Temporal Properties are Expressible Without the Next-time Operator. Information Processing Letters 63(5), 243–246 (1997)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Poitrenaud, D., Pradat-Peyre, J.-F.: Pre- and Post-agglomerations for LTL Model Checking. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 387–408. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    PROD. Pr/T-net reachability analysis tool. Helsinki Univerity of Technology, http://www.tcs.hut.fi/Software/prod/
  11. 11.
    Rakow, A.: Slicing Petri nets with an Application to Workflow Verification. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds.) SOFSEM 2008. LNCS, vol. 4910, pp. 436–447. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Rakow, A.: Slicing Petri Nets. Technical Report, Carl von Ossietzky Universität Oldenburg, 20 pages (2007), http://parsys.informatik.uni-oldenburg.de/pubs/SlPN_tr.pdf
  13. 13.
    Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  14. 14.
    Vasudevan, S., Emerson, E.A., Abraham, J.A.: Efficient model checking of hardware using conditioned slicing. In: Proc. of the 4th International Workshop on Automated Verification of Critical Systems, AVOCS 2004. Electronic Notes in Theoretical Computer Science, vol. 128(6), pp. 279–294. Elsevier Science Publishers (2004)Google Scholar
  15. 15.
    Vasudevan, S., Emerson, E.A., Abraham, J.A.: Improved Verification of Hardware Designs Through Antecedant Conditioned Slicing. International Journal of Software Tools and Technology Transfer (STTT) 9(1), 89–101 (2007)CrossRefGoogle Scholar
  16. 16.
    Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Press, Piscataway (1981)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Astrid Rakow
    • 1
  1. 1.Universität OldenburgGermany

Personalised recommendations