Advertisement

Parametric Model Checking with VerICS

  • Michał Knapik
  • Artur Niewiadomski
  • Wojciech Penczek
  • Agata Półrola
  • Maciej Szreter
  • Andrzej Zbrzezny
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Model Check Mutual Exclusion Propositional Formula Computation Tree Logic Bound Model Check 
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.
    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. 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. 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. 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. 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. 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)CrossRefGoogle Scholar
  7. 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)CrossRefGoogle Scholar
  8. 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)CrossRefGoogle Scholar
  9. 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)CrossRefGoogle Scholar
  10. 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. 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. 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. 13.
    Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)zbMATHGoogle Scholar
  14. 14.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Eng. 23(5), 279–295 (1997)CrossRefGoogle Scholar
  15. 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)CrossRefGoogle Scholar
  16. 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. 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)MathSciNetzbMATHGoogle Scholar
  18. 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. 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. 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)CrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 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)CrossRefGoogle Scholar
  23. 23.
  24. 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)MathSciNetzbMATHGoogle Scholar
  25. 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)CrossRefGoogle Scholar
  26. 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)CrossRefGoogle Scholar
  27. 27.
    OMG. Unified Modeling Language (2007), http://www.omg.org/spec/UML/2.1.2
  28. 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)CrossRefGoogle Scholar
  29. 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. 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. 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)MathSciNetzbMATHGoogle Scholar
  32. 32.
    Półrola, A., Penczek, W.: Minimization algorithms for time Petri nets. Fundamenta Informaticae 60(1-4), 307–331 (2004)MathSciNetzbMATHGoogle Scholar
  33. 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)CrossRefGoogle Scholar
  34. 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)CrossRefGoogle Scholar
  35. 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)CrossRefGoogle Scholar
  36. 36.
    Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)MathSciNetzbMATHGoogle Scholar
  37. 37.
    Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4), 513–531 (2008)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Michał Knapik
    • 1
  • Artur Niewiadomski
    • 2
  • Wojciech Penczek
    • 1
    • 2
  • Agata Półrola
    • 3
  • Maciej Szreter
    • 1
  • Andrzej Zbrzezny
    • 4
  1. 1.Institute of Computer SciencePASWarszawaPoland
  2. 2.ICSSiedlce UniversitySiedlcePoland
  3. 3.FMCSUniversity of ŁódźŁódźPoland
  4. 4.IMCSJan Długosz UniversityCzȩstochowaPoland

Personalised recommendations