Stubborn Sets, Frozen Actions, and Fair Testing

• Autorzy: Valmari Antti , Vogler Walter

Identyfikatory

DOI

10.3233/FI-2021-2001

• Języki publikacji: EN

Abstrakty

EN

Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based on recognizing the terminal strong components of the reduced state space and, if necessary, expanding the stubborn sets used in their roots. In an earlier study it was pointed out that if the system may execute a cycle consisting of only invisible actions and that cycle is concurrent with the rest of the system in a non-obvious way, then the method may be fooled to construct all states of the full parallel composition. This problem is solved in this study by a method that “freezes” the actions in the cycle. The new method also preserves fair testing equivalence, making it usable for the verification of many progress properties.

Słowa kluczowe

EN

fair testing; ignoring problem; partial order methods; safety properties; stubborn sets

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 178, nr 1/2
• Strony: 139--172
• Opis fizyczny: Bibliogr. 29 poz., rys.

Twórcy

autor

Valmari Antti

• Faculty of Information Technology, University of Jyväskylä, P.O. Box 35 (Ag C416.2), FI-40014 University of Jyväskylä, Jyväskylä, Finland

autor

Vogler Walter

• Institut für Informatik, University of Augsburg, D-86135 Augsburg, Germany

Bibliografia

• [1] Clarke EM, Grumberg O, Peled DA. Model checking. MIT Press, 1999. ISBN 978-0-262-03270-4.
• [2] Peled DA. All from One, One for All: on Model Checking Using Representatives. In: Courcoubetis C (ed.), Computer Aided Verification, 5th International Conference, CAV ’93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science. Springer, 1993 pp. 409-423. doi:10.1007/3-540-56922-7_34.
• [3] Peled DA. Partial order reduction: Linear and branching temporal logics and process algebras. In: Peled DA, Pratt VR, Holzmann GJ (eds.), Partial Order Methods in Verification, Proceedings of a DIMACS Workshop, Princeton, New Jersey, USA, July 24-26, 1996, volume 29 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. DIMACS/AMS, 1996 pp. 233-258.
• [4] Godefroid P. Using Partial Orders to Improve Automatic Verification Methods. In: Clarke EM, Kurshan RP (eds.), Computer-Aided Verification, Proceedings of a DIMACS Workshop 1990, New Brunswick, New Jersey, USA, June 18-21, 1990, volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. DIMACS/AMS, 1990 pp. 321-340.
• [5] Godefroid P. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, 1996. ISBN 3-540-60761-7. doi:10.1007/3-540-60761-7.
• [6] Valmari A. Error Detection by Reduced Reachability Graph Generation. In: Proceedings of the 9th European Workshop on Application and Theory of Petri Nets. 1988 pp. 95-122.
• [7] Valmari A. The State Explosion Problem. In: Reisig W, Rozenberg G (eds.), Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science. Springer, 1996 pp. 429-528. doi:10.1007/3-540-65306-6_21.
• [8] Vogler W. Modular Construction and Partial Order Semantics of Petri Nets, volume 625 of Lecture Notes in Computer Science. Springer, 1992. ISBN 3-540-55767-9. doi:10.1007/3-540-55767-9.
• [9] Rensink A, Vogler W. Fair testing. Inf. Comput., 2007. 205(2):125-198. doi:10.1016/j.ic.2006.06.002.
• [10] Valmari A, Vogler W. Fair Testing and Stubborn Sets. STTT, 2017. doi:10.1007/s10009-017-0481-2.
• [11] Valmari A, Hansen H. Stubborn Set Intuition Explained. In: Cabac L, Kristensen LM, Rölke H (eds.), Proceedings of the International Workshop on Petri Nets and Software Engineering 2016, including the International Workshop on Biological Processes & Petri Nets 2016 co-located with the 37th International Conference on Application and Theory of Petri Nets and Concurrency Petri Nets 2016 and the 16th International Conference on Application of Concurrency to System Design ACSD 2016, Toruń, Poland, June 20-21, 2016, volume 1591 of CEUR Workshop Proceedings. CEUR-WS.org, 2016 pp. 213-232.
• [12] Valmari A, Hansen H. Stubborn Set Intuition Explained. Trans. Petri Nets and Other Models of Concurrency, 2017. 12:140-165. doi:10.1007/978-3-662-55862-1_7.
• [13] Valmari A. Stubborn sets for reduced state space generation. In: Rozenberg G (ed.), Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 of Lecture Notes in Computer Science. Springer, 1989 pp. 491-515. doi:10.1007/3-540-53863-1_36.
• [14] Valmari A. Stubborn set methods for process algebras. In: Peled DA, Pratt VR, Holzmann GJ (eds.), Partial Order Methods in Verification, Proceedings of a DIMACS Workshop, Princeton, New Jersey, USA, July 24-26, 1996, volume 29 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. DIMACS/AMS, 1996 pp. 213-232.
• [15] Valmari A, Vogler W. Fair Testing and Stubborn Sets. In: Bosnacki D, Wijs A (eds.), Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings, volume 9641 of Lecture Notes in Computer Science. Springer, 2016 pp. 225-243. doi:10.1007/978-3-319-32582-8_16.
• [16] Valmari A. More Stubborn Set Methods for Process Algebras. In: Gibson-Robinson T, Hopcroft PJ, Lazic R (eds.), Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, volume 10160 of Lecture Notes in Computer Science. Springer, 2017 pp. 246-271. doi:10.1007/978-3-319-51046-0_13.
• [17] Valmari A. Stubborn Sets with Frozen Actions. In: Hague M, Potapov I (eds.), Reachability Problems, 11th International Workshop, RP 2017, volume 10506 of Lecture Notes in Computer Science. 2017 pp. 160-175. doi:10.1007/978-3-319-67089-8_12.
• [18] Evangelista S, Pajault C. Solving the ignoring problem for partial order reduction. STTT, 2010. 12(2):155-170. doi:10.1007/s10009-010-0137-y.
• [19] Siegel SF. What’s Wrong with On-the-Fly Partial Order Reduction. In: Dillig I, Tasiran S (eds.), Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, volume 11562 of Lecture Notes in Computer Science. Springer, 2019 pp. 478-495. doi:10.1007/978-3-030-25543-5_27. URL https://doi.org/10.1007/978-3-030-25543-5_27.
• [20] Holzmann GJ. The SPIN Model Checker - primer and reference manual. Addison-Wesley, 2004. ISBN 978-0-321-22862-8.
• [21] Neele T, Valmari A, Willemse TAC. The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, vol. 12077 of LNCS, Springer, 2020 pp. 482-501. doi:10.1007/978-3-030-45231-5_25.
• [22] Mazurkiewicz AW. Trace Theory. In: Brauer W, Reisig W, Rozenberg G (eds.), Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8-19. September 1986, volume 255 of Lecture Notes in Computer Science. Springer, 1986 pp. 279-324. doi:10.1007/3-540-17906-2_30.
• [23] Manna Z, Pnueli A. The temporal logic of reactive and concurrent systems - specification. Springer, 1992. ISBN 978-3-540-97664-6.
• [24] Tarjan RE. Depth-First Search and Linear Graph Algorithms. SIAM J. Comput., 1972. 1(2):146-160. doi:10.1137/0201010.
• [25] Eve J, Kurki-Suonio R. On Computing the Transitive Closure of a Relation. Acta Inf., 1977. 8:303-314. doi:10.1007/BF00271339.
• [26] Gabow HN. Path-based depth-first search for strong and biconnected components. Inf. Process. Lett., 2000. 74(3-4):107-114. doi:10.1016/S0020-0190(00)00051-X.
• [27] Valmari A. A State Space Tool for Concurrent System Models Expressed in C++. In: Nummenmaa J, Sievi-Korte O, Mäkinen E (eds.), Proceedings of the 14th Symposium on Programming Languages and Software Tools (SPLST’15), Tampere, Finland, October 9-10, 2015, volume 1525 of CEUR Workshop Proceedings. CEUR-WS.org, 2015 pp. 91-105.
• [28] Valmari A. Stop It, and Be Stubborn! ACM Trans. Embedded Comput. Syst., 2017. 16(2):46:1-46:26. doi:10.1145/3012279.
• [29] Valmari A, Hansen H. Progress Checking for Dummies. In: Howar F, Barnat J (eds.), Proceedings of Formal Methods for Industrial Critical Systems, volume 11119 of Lecture Notes in Computer Science. Springer, 2018 pp. 115-130. doi:10.1007/978-3-030-00244-2_8.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).