nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.08.2016 | SPIN 2013

Guard-based partial-order reduction

verfasst von: Alfons Laarman, Elwin Pater, Jaco van de Pol, Henri Hansen

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper aims at making partial-order reduction independent of the modeling language. To this end, we present a guard-based method which is a general-purpose implementation of the stubborn set method. We approach the implementation through so-called necessary enabling sets and do-not-accord sets, and give an algorithm suitable for an abstract model checking interface. We also introduce necessary disabling sets and heuristics to produce smaller stubborn sets and thus better reduction at low costs. We explore the effect of these methods using an implementation in the model checker LTSmin. We experiment with partial-order reduction on a number of Promela models, on benchmarks from the BEEM database in the DVE language, and with several with LTL properties. The efficiency of the heuristic algorithm is established by a comparison to the subset-minimal Deletion algorithm and the simple closure algorithm. We also compare our results to the Spin model checker. While the reductions take longer, they are consistently better than Spin ’s ample set and often surpass the upper bound for the process-based ample sets, established empirically earlier on BEEM models.

Vorheriger Artikel Efficient model-checking of weighted CTL with upper-bound constraints

Nächster Artikel Guided search for hybrid systems based on coarse-grained space abstractions

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

http://fmt.cs.utwente.nl/tools/ltsmin/.

http://spinroot.com.

http://www.albertolluch.com/research/promelamodels.

Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, Orna (ed.) CAV, vol. 1254 of LNCS, pp. 340–351. Springer, New York (1997)

van der Berg, F.I., Laarman, A.W.: SpinS: Extending LTSmin with Promela through SpinJa. In: PDMC 2012, London, UK, ENTCS. Springer, New York (2012)

Blom, S.C.C., van de Pol, J.C., Weber, M.: LTSmin: distributed and symbolic reachability. In: CAV, vol. 6174 of LNCS, pp. 354–359. Springer, New York (2010)

Chu, D.H., Jaffar, J.: A framework to synergize partial order reduction with state interpolation. In: Yahav, E. (ed.) HVC, vol. 8855 of LNCS, pp. 171–187. Springer, New York (2014)

Clarke, E.M.: The birth of model checking. In: 25 Years of Model Checking, pp. 1–26. Springer, Berlin (2008)

Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: CAV, vol. 531 of LNCS, pp. 233–242. Springer, New York (1990)

Dong, Y., Du, X., Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Sokolsky, O., Stark, E.W.: Fighting livelock in the i-protocol: a comparative study of verification tools. In: Rance Cleaveland, W. (ed.) TACAS, vol. 1579 of LNCS, pp. 74–88. Springer, New York (1999)

Groote, J.F., et al.: The mCRL2 toolset. In: Proceedings of the International Workshop on Advanced Software Development Tools and Techniques, WASDeTT (2008)

Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In: ATVA, LNCS 7561, pp. 269–283. Springer, New York (2012)

10.

Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. STTT 12, 155–170 (2010)CrossRef

11.

Geldenhuys, J., Hansen, H., Valmari, A.: Exploring the scope for partial order reduction. In: ATVA’09, LNCS, pp. 39–53. Springer, New York (2009)

12.

Godefroid, P.: Using partial orders to improve automatic verification methods. In: CAV, vol. 531 of LNCS, pp. 176–185. Springer, New York (1990)

13.

Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, New York (1996)CrossRefMATH

14.

Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods. In: CAV, vol. 697 of LNCS, pp. 438–449. Springer, New York (1993)

15.

Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. FMSD 2, 149–164 (1993)MATH

16.

Hansen, H., Lin, S.W., Liu, Y., Nguyen, T.K., Sun, J.: Diamonds are a girl’s best friend: Partial order reduction for timed automata with abstractions. In: Biere, A., Bloem, R. (eds.) CAV, vol. 8559 of LNCS, pp. 391–406. Springer, New York (2014)

17.

Holzmann, G.J.: The model checker SPIN. IEEE TSE 23, 279–295 (1997)

18.

Holzmann, G.J., Peled, D.: An improvement in formal verification. In: IFIP WG6.1 ICFDT VII, pp. 197–211. Chapman & Hall Ltd, London (1995)

19.

Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: SPIN, pp. 23–32. American Mathematical Society (1996)

20.

Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: CAV, LNCS, pp. 398–413. Springer, New York (2009)

21.

Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: REX Workshop, vol. 354 of LNCS, pp. 489–507. Springer, Berlin (1988)

22.

Kokkarinen, I., Peled, D., Valmari, A.: Relaxed visibility enhances partial order reduction. In: Grumberg, O. (ed.) CAV, vol. 1254 of LNCS, pp. 328–339. Springer, New York (1997)

23.

Konnov, I., Letichevsky Jr, O.A.: Model checking GARP protocol using Spin and VRS. International Workshop on Automata, Algorithms, Information Technologies (2010)

24.

Laarman, A.W., Wijs, A.J.: Partial-order reduction for multi-core LTL model checking. In: Yahav, V. (ed.) HVC 2014, vol. 8855 of LNCS, pp. 267–283. Springer, New York (2014)

25.

Laarman, A.W.: Scalable multi-core model checking. PhD thesis, University of Twente (2014)

26.

Laarman, A.W., Fárago, D.: Improved on-the-fly livelock detection. In: NFM, accepted for publication in LNCS. Springer, New York (2013)

27.

Laarman, A.W., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.C.: Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In: Sharygina, N., Veith, H. (eds.) CAV, vol. 8044 of LNCS, pp. 968–983. Springer, New York (2013)

28.

Laarman, A.W., Pater, E., van de Pol, J.C., Weber, M.: Guard-based partial-order reduction. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Model Checking Software, vol. 7976 of LNCS, pp. 227–245. Springer, New York (2013)CrossRef

29.

Laarman, A.W., van de Pol, J.C., Weber, M.: Parallel recursive state compression for free. In: SPIN, LNCS, pp. 38–56. Springer, New York (2011)

30.

Laarman, A.W., van de Pol, J.C., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: NFM, LNCS 6617, pp. 506–511. Springer, New York (2011)

31.

Larsen, K., Pettersson, P., Yi, W.: Uppaal in a Nutshell. STTT 1, 134–152 (1997)CrossRefMATH

32.

Lehmann, A., Lohmann, N., Wolf, K.: Stubborn sets for simple linear time properties. In: Application and Theory of Petri Nets, vol. 7347 of LNCS, pp. 228–247. Springer, New York (2012)

33.

Meijer, J., Kant, G., Blom, S.C.C., van de Pol, J.C.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) Hardware and Software: Verification and Testing, vol. 8855 of LNCS, pp. 204–219. Springer, New York (2014)

34.

Overman, W.T.: Verification of concurrent systems: function and timing. PhD thesis, University of California, Los Angeles (1981, AAI8121023)

35.

Peng, S.O., Thomas, E.M.: Filtered beam search in scheduling? Int. J. Prod. Res. 26(1), 35–62 (1988)CrossRef

36.

Pater, E.: Partial order reduction for PINS. Master’s thesis (2011)

37.

Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Proceedings of SPIN Workshop, volume 4595 of LNCS, pp. 263–267. Springer, New York (2007)

38.

Peled, D.: All from one, one for all: on model checking using representatives. In: CAV, pp. 409–423. Springer, New York (1993)

39.

Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: CAV, vol. 818 of LNCS, pp. 377–390. Springer, New York (1994)

40.

Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society (1977)

41.

Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: TACAS, vol. 3440 of LNCS, pp. 174–190. Springer, New York (2005)

42.

Sharma, A.: End to end verification and validation with SPIN. CoRR (2013, abs/1302.4796)

43.

Siegel, S.F.: Reexamining two results in partial order reduction. Technical report, University of Delaware (2011)

44.

Siegel, S.F.: Transparent partial order reduction. FMSD 40(1), 1–19 (2012)MATH

45.

Valmari, A.: Error detection by reduced reachability graph generation. In: APN, pp. 95–112 (1988)

46.

Valmari, A.: Heuristics for lazy state generation speeds up analysis of concurrent systems. In: STeP-88, vol. 2, pp. 640–650. Helsinki (1988)

47.

Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: PARLE, vol. 366 of LNCS, pp. 89–103. Springer, New York (1989)

48.

Valmari A.: A stubborn attack on state explosion. In: CAV, LNCS, pp. 156–165. Springer, New York (1991)

49.

Valmari, A.: Stubborn sets for reduced state space generation. In: ICATPN/APN’90, pp. 491–515. Springer, New York (1991)

50.

Valmari, A.: The state explosion problem. In: LPN, pp. 429–528. Springer, New York (1998)

51.

Valmari, A., Hansen, H.: Can stubborn sets be optimal? In: Lilius, J., Penczek, W. (eds.) ATPN, vol. 6128 of LNCS, pp. 43–62. Springer, New York (2010)

52.

Valmari, A.: Stubborn set methods for process algebras. In: DIMACS Workshop on Partial Order Methods in Verification, pp. 213–231. AMS Press Inc, Brooklyn (1997)

53.

Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332–344. IEEE (1986)

54.

Varpaaniemi, K.: Finding small stubborn sets automatically. Proceedings of the Eleventh International Symposium on Computer and Information Sciences, ISCIS XI, pp. 133–142. Middle East Technical University, Ankara (1996)

55.

Varpaaniemi, K.: On the stubborn set method in reduced state space generation. PhD thesis, Helsinki University of Technology (1998)

56.

Wehrle, M., Helmert, M.: Efficient stubborn sets: generalized algorithms and selection strategies. In: International Conference on Automated Planning and Scheduling. AAAI Publications, Canada (2014)

Titel: Guard-based partial-order reduction
verfasst von: Alfons Laarman
Elwin Pater
Jaco van de Pol
Henri Hansen
Publikationsdatum: 01.08.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 4/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-014-0363-9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 4/2016

Preface of the special issue on Model Checking of Software

Guided search for hybrid systems based on coarse-grained space abstractions

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

Verifying a quantitative relaxation of linearizability via refinement

Efficient model-checking of weighted CTL with upper-bound constraints

Model checking unbounded concurrent lists