Skip to main content
SpringerLink
Log in

Parametric Model Checking with VerICS

  • Chapter
Transactions on Petri Nets and Other Models of Concurrency IV

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 6550))

Abstract

The paper presents the verification system verICS, extended with the three new modules aimed at parametric verification of Elementary Net Systems, Distributed Time Petri Nets, and a subset of UML. All the modules exploit Bounded Model Checking for verifying parametric reachability and the properties specified in the logic PRTECTL – the parametric extension of the existential fragment of CTL.

Partly supported by the Polish Ministry of Science and Higher Education under the grants No. N N206 258035 and N N516 370436.

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

Access this chapter

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 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Dill, D.: Model checking for real-time systems. In: Proc. of the 5th Symp. on Logic in Computer Science (LICS 1990), pp. 414–425. IEEE Computer Society Press, Los Alamitos (1990)

    Google Scholar 

  2. Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS 1992), pp. 157–166. IEEE Computer Society Press, Los Alamitos (1992)

    Google Scholar 

  3. Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., Weise, C.: New generation of Uppaal. In: Proc. of the Int. Workshop on Software Tools for Technology Transfer (1998)

    Google Scholar 

  4. Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research 42(14) (2004)

    Google Scholar 

  5. Bruyére, V., Dall’Olio, E., Raskin, J.-F.: Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic 9(2) (2008)

    Google Scholar 

  6. Christensen, S., Jørgensen, J., Kristensen, L.: Design/CPN - a computer tool for coloured Petri nets. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 209–223. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  7. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Dembinski, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS: A tool for verifying timed automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Dierks, H., Tapken, J.: MOBY/DC - A tool for model-checking parametric real-time specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 271–277. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Diethers, K., Goltz, U., Huhn, M.: Model checking UML statecharts with time. In: Proc. of the Workshop on Critical Systems Development with UML (CSDUML 2002), Technische Universität München, pp. 35–52 (2002)

    Google Scholar 

  11. Dubrovin, J., Junttila, T.: Symbolic model checking of hierarchical UML state machines. Technical Report HUT-TCS-B23, Helsinki Institute of Technology, Espoo, Finland (2007)

    Google Scholar 

  12. Emerson, E.A., Trefler, R.: Parametric quantitative temporal reasoning. In: Proc. of the 14th Symp. on Logic in Computer Science (LICS 1999), July 1999, pp. 336–343. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  13. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)

    MATH  Google Scholar 

  14. Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  15. Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 189–203. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dynamic and hierarchical UML state machines. In: Proc. of the 3rd Int. Workshop on Model Design and Validation (MoDeVa 2006), pp. 94–110. CEA (2006)

    Google Scholar 

  17. Kacprzak, M., Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1-4), 313–328 (2008)

    MathSciNet  MATH  Google Scholar 

  18. Kacprzak, M., Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2008 - a model checker for time Petri nets and high-level languages. In: Proc. of Int. Workshop on Petri Nets and Software Engineering (PNSE 2009), pp. 119–132. University of Hamburg (2009)

    Google Scholar 

  19. Knapik, M., Szreter, M., Penczek, W.: Bounded Parametric Model Checking for Elementary Net Systems. In: Jensen, K., Donatelli, S., Koutny, M. (eds.) ToPNoC IV. LNCS, vol. 6550, pp. 42–71. Springer, Heidelberg (2011)

    Google Scholar 

  20. Knapp, A., Merz, S., Rauh, C.: Model checking - timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–416. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Lilius, J., Paltor, I.: vUML: A tool for verifying UML models. In: Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering (ASE 1999), pp. 255–258. IEEE Computer Society Press, Los Alamitos (1999)

    Chapter  Google Scholar 

  22. Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: A parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. MiniSat (2006), http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat

  24. Niewiadomski, A., Penczek, W., Szreter, M.: A new approach to model checking of UML state machines. Fundamenta Informaticae 93(1-3), 289–303 (2009)

    MathSciNet  MATH  Google Scholar 

  25. Niewiadomski, A., Penczek, W., Szreter, M.: Towards checking parametric reachability for UML state machines. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 319–330. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  26. Okawa, Y., Yoneda, T.: Symbolic CTL model checking of time Petri nets. Electronics and Communications in Japan, Scripta Technica 80(4), 11–20 (1997)

    Article  Google Scholar 

  27. OMG. Unified Modeling Language (2007), http://www.omg.org/spec/UML/2.1.2

  28. Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  29. Penczek, W., Półrola, A., Woźna, B., Zbrzezny, A.: Bounded model checking for reachability testing in time Petri nets. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2004). Informatik-Berichte, vol. 170(1), pp. 124–135. Humboldt University (2004)

    Google Scholar 

  30. Penczek, W., Pòłrola, A., Zbrzezny, A.: SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets. In: Jensen, K., Donatelli, S., Koutny, M. (eds.) ToPNoC IV. LNCS, vol. 6550, pp. 72–97. Springer, Heidelberg (2011)

    Google Scholar 

  31. Penczek, W., Woźna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae 51(1-2), 135–156 (2002)

    MathSciNet  MATH  Google Scholar 

  32. Półrola, A., Penczek, W.: Minimization algorithms for time Petri nets. Fundamenta Informaticae 60(1-4), 307–331 (2004)

    MathSciNet  MATH  Google Scholar 

  33. Spelberg, R.L., Toetenel, H., Ammerlaan, M.: Partition refinement in real-time model checking. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 143–157. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  34. Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of time petri nets with stopwatches using the state-class graph. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 280–294. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  35. Virbitskaite, I.B., Pokozy, E.A.: A partial order method for the verification of time petri nets. In: Ciobanu, G., Păun, G. (eds.) FCT 1999. LNCS, vol. 1684, pp. 547–558. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  36. Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)

    MathSciNet  MATH  Google Scholar 

  37. Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4), 513–531 (2008)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, PAS, Ordona 21, 01-237, Warszawa, Poland

    Michał Knapik, Wojciech Penczek & Maciej Szreter

  2. ICS, Siedlce University, 3 Maja 54, 08-110, Siedlce, Poland

    Artur Niewiadomski & Wojciech Penczek

  3. FMCS, University of Łódź, Banacha 22, 90-238, Łódź, Poland

    Agata Półrola

  4. IMCS, Jan Długosz University, Armii Krajowej 13/15, 42-200, Czȩstochowa, Poland

    Andrzej Zbrzezny

Authors
  1. Michał Knapik
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Artur Niewiadomski
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wojciech Penczek
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Agata Półrola
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Maciej Szreter
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Andrzej Zbrzezny
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Aarhus, Faculty of Science, IT-parken, Aabogade 34, 8200, Aarhus N, Denmark

    Kurt Jensen

  2. Computer Science Department, University of Turin, Corso Svizzera 185, 10149, Turin, Italy

    Susanna Donatelli

  3. School of Computing Science, Newcastle upon Tyne, Newcastle University, NE1 7RU, UK

    Maciej Koutny

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Knapik, M., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., Zbrzezny, A. (2010). Parametric Model Checking with VerICS . In: Jensen, K., Donatelli, S., Koutny, M. (eds) Transactions on Petri Nets and Other Models of Concurrency IV. Lecture Notes in Computer Science, vol 6550. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18222-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-18222-8_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-18221-1

  • Online ISBN: 978-3-642-18222-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation