Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Software Engineering for Resilient Systems

SERENE 2013: Software Engineering for Resilient Systems pp 64–78Cite as

Optimizing Verification of Structurally Evolving Algebraic Petri Nets

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8166))

Abstract

System models are subject to evolve during the development life cycle, along which an initial version goes through a series of evolutions, generally aimed at progressively reaching all the requested qualities (completeness, correctness etc.). Among the existing development methodologies the iterative and incremental one has been proved to be efficient for system development but lacks of support for an adequate verification process. When considering Algebraic Petri nets (APNs) for modeling and model checking for verification, all the proofs must be redone after each iteration which is impractical both in terms of time and space. In this work, we introduce an Algebraic Petri net slicing technique that optimizes the model checking of static or structurally evolving APN models. Furthermore, our approach is proposing a classification of evolutions dedicated to the improvement of model checking.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Buchs, D., Hostettler, S., Marechal, A., Risoldi, M.: AlPiNA: A symbolic model checker. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 287–296. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  2. Burch, J.R., Clarke, E., McMillan, K.L., Dill, D., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 428–439 (1990)

    Google Scholar 

  3. Chang, J., Richardson, D.J.: Static and dynamic specification slicing. In: Proceedings of the Fourth Irvine Software Symposium (1994)

    Google Scholar 

  4. Christensen, S., Petrucci, L.: Towards a modular analysis of coloured petri nets. In: Jensen, K. (ed.) ICATPN 1992. LNCS, vol. 616, pp. 113–133. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  5. Christensen, S., Petrucci, L.: Modular analysis of petri nets. The Computer Journal 43, 2000 (2000)

    Article  Google Scholar 

  6. Er, S.P.: Invariant property preserving extensions of elementary petri nets. Technical report, Technische Universitat Berlin (1997)

    Google Scholar 

  7. Khan, Y.I.: Optimizing verification of structurally evolving algebraic petri nets. Technical Report TR-LASSY-13-03, University of Luxembourg (2012)

    Google Scholar 

  8. Khan, Y.I., Risoldi, M.: Language enrichment for resilient MDE. In: Avgeriou, P. (ed.) SERENE 2012. LNCS, vol. 7527, pp. 76–90. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  9. Khan, Y.I., Risoldi, M.: Optimizing algebraic petri net model checking by slicing. In: International Workshop on Modeling and Business Environments (ModBE 2013, associated with Petri Nets 2013) (2013)

    Google Scholar 

  10. Lakos, C., Petrucci, L.: Modular state spaces and place fusion. In: International Workshop on Petri Nets and Software Engineering (PNSE 2007, associated with Petri Nets 2007), pp. 175–190 (2007)

    Google Scholar 

  11. Larman, C., Basili, V.: Iterative and incremental developments. A brief history. Computer 36(6), 47–56 (2003)

    Article  Google Scholar 

  12. Lee, W.J., Kim, H.N., Cha, S.D., Kwon, Y.R.: A slicing-based approach to enhance petri net reachability analysis. Journal of Research Practices and Information Technology 32, 131–143 (2000)

    Google Scholar 

  13. Lucio, L., Syriani, E., Amrani, M., Zhang, Q., Vangheluwe, H.: Invariant preservation in iterative modeling. In: Proceedings of the ME 2012 Workshop (2012)

    Google Scholar 

  14. Llorens, M., Oliver, J., Silva, J., Tamarit, S., Vidal, G.: Dynamic slicing techniques for petri nets. Electron. Notes Theor. Comput. Sci. 223, 153–165 (2008)

    Article  Google Scholar 

  15. Padberg, J., Gajewsky, M., Ermel, C.: Rule-based refinement of high-level nets preserving safety properties. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 221–238. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Rakow, A.: Slicing and Reduction Techniques for Model Checking Petri Nets. PhD thesis, University of Oldenburg (2011)

    Google Scholar 

  18. Rakow, A.: Safety slicing petri nets. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 268–287. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Reisig, W.: Petri nets and algebraic specifications. Theor. Comput. Sci. 80(1), 1–34 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  20. Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, ICSE 1981, pp. 439–449. IEEE Press, Piscataway (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory of Advanced Software Systems, University of Luxembourg, 6, rue R. Coudenhove-Kalergi, Luxembourg

    Yasir Imtiaz Khan

Authors
  1. Yasir Imtiaz Khan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Systems and Networks, National Aerospace University, 17, Chkalov Street, 61070, Kharkiv, Ukraine

    Anatoliy Gorbenko  & Vyacheslav Kharchenko  & 

  2. School of Computing Science, Newcastle University, Claremont Tower, NE1 7RU, Newcastle upon Tyne, UK

    Alexander Romanovsky

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Khan, Y.I. (2013). Optimizing Verification of Structurally Evolving Algebraic Petri Nets. In: Gorbenko, A., Romanovsky, A., Kharchenko, V. (eds) Software Engineering for Resilient Systems. SERENE 2013. Lecture Notes in Computer Science, vol 8166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40894-6_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40894-6_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40893-9

  • Online ISBN: 978-3-642-40894-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation