Supporting domain-specific state space reductions through local partial-order reduction

Peter Bokor, Johannes Kinder, Marco Serafini, Neeraj Suri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

Model checkers offer to automatically prove safety and liveness properties of complex concurrent software systems, but they are limited by state space explosion. Partial-Order Reduction (POR) is an effective technique to mitigate this burden. However, applying existing notions of POR requires to verify conditions based on execution paths of unbounded length, a difficult task in general. To enable a more intuitive and still flexible application of POR, we propose local POR (LPOR). LPOR is based on the existing notion of statically computed stubborn sets, but its locality allows to verify conditions in single states rather than over long paths. As a case study, we apply LPOR to message-passing systems. We implement it within the Java Pathfinder model checker using our general Java-based LPOR library. Our experiments show significant reductions achieved by LPOR for model checking representative message-passing protocols and, maybe surprisingly, that LPOR can outperform dynamic POR.

Original languageEnglish
Title of host publication2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings
Pages113-122
Number of pages10
DOIs
Publication statusPublished - 1 Dec 2011
Externally publishedYes
Event2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011 - Lawrence, KS, United States
Duration: 6 Nov 201110 Nov 2011

Other

Other2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011
CountryUnited States
CityLawrence, KS
Period6/11/1110/11/11

Fingerprint

Message passing
Model checking
Explosions
Network protocols
Experiments

ASJC Scopus subject areas

  • Software

Cite this

Bokor, P., Kinder, J., Serafini, M., & Suri, N. (2011). Supporting domain-specific state space reductions through local partial-order reduction. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings (pp. 113-122). [6100044] https://doi.org/10.1109/ASE.2011.6100044

Supporting domain-specific state space reductions through local partial-order reduction. / Bokor, Peter; Kinder, Johannes; Serafini, Marco; Suri, Neeraj.

2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings. 2011. p. 113-122 6100044.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bokor, P, Kinder, J, Serafini, M & Suri, N 2011, Supporting domain-specific state space reductions through local partial-order reduction. in 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings., 6100044, pp. 113-122, 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Lawrence, KS, United States, 6/11/11. https://doi.org/10.1109/ASE.2011.6100044
Bokor P, Kinder J, Serafini M, Suri N. Supporting domain-specific state space reductions through local partial-order reduction. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings. 2011. p. 113-122. 6100044 https://doi.org/10.1109/ASE.2011.6100044
Bokor, Peter ; Kinder, Johannes ; Serafini, Marco ; Suri, Neeraj. / Supporting domain-specific state space reductions through local partial-order reduction. 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings. 2011. pp. 113-122
@inproceedings{f883a2a732ea436b845d751b3be80c5a,
title = "Supporting domain-specific state space reductions through local partial-order reduction",
abstract = "Model checkers offer to automatically prove safety and liveness properties of complex concurrent software systems, but they are limited by state space explosion. Partial-Order Reduction (POR) is an effective technique to mitigate this burden. However, applying existing notions of POR requires to verify conditions based on execution paths of unbounded length, a difficult task in general. To enable a more intuitive and still flexible application of POR, we propose local POR (LPOR). LPOR is based on the existing notion of statically computed stubborn sets, but its locality allows to verify conditions in single states rather than over long paths. As a case study, we apply LPOR to message-passing systems. We implement it within the Java Pathfinder model checker using our general Java-based LPOR library. Our experiments show significant reductions achieved by LPOR for model checking representative message-passing protocols and, maybe surprisingly, that LPOR can outperform dynamic POR.",
author = "Peter Bokor and Johannes Kinder and Marco Serafini and Neeraj Suri",
year = "2011",
month = "12",
day = "1",
doi = "10.1109/ASE.2011.6100044",
language = "English",
isbn = "9781457716393",
pages = "113--122",
booktitle = "2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings",

}

TY - GEN

T1 - Supporting domain-specific state space reductions through local partial-order reduction

AU - Bokor, Peter

AU - Kinder, Johannes

AU - Serafini, Marco

AU - Suri, Neeraj

PY - 2011/12/1

Y1 - 2011/12/1

N2 - Model checkers offer to automatically prove safety and liveness properties of complex concurrent software systems, but they are limited by state space explosion. Partial-Order Reduction (POR) is an effective technique to mitigate this burden. However, applying existing notions of POR requires to verify conditions based on execution paths of unbounded length, a difficult task in general. To enable a more intuitive and still flexible application of POR, we propose local POR (LPOR). LPOR is based on the existing notion of statically computed stubborn sets, but its locality allows to verify conditions in single states rather than over long paths. As a case study, we apply LPOR to message-passing systems. We implement it within the Java Pathfinder model checker using our general Java-based LPOR library. Our experiments show significant reductions achieved by LPOR for model checking representative message-passing protocols and, maybe surprisingly, that LPOR can outperform dynamic POR.

AB - Model checkers offer to automatically prove safety and liveness properties of complex concurrent software systems, but they are limited by state space explosion. Partial-Order Reduction (POR) is an effective technique to mitigate this burden. However, applying existing notions of POR requires to verify conditions based on execution paths of unbounded length, a difficult task in general. To enable a more intuitive and still flexible application of POR, we propose local POR (LPOR). LPOR is based on the existing notion of statically computed stubborn sets, but its locality allows to verify conditions in single states rather than over long paths. As a case study, we apply LPOR to message-passing systems. We implement it within the Java Pathfinder model checker using our general Java-based LPOR library. Our experiments show significant reductions achieved by LPOR for model checking representative message-passing protocols and, maybe surprisingly, that LPOR can outperform dynamic POR.

UR - http://www.scopus.com/inward/record.url?scp=84855435153&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84855435153&partnerID=8YFLogxK

U2 - 10.1109/ASE.2011.6100044

DO - 10.1109/ASE.2011.6100044

M3 - Conference contribution

SN - 9781457716393

SP - 113

EP - 122

BT - 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings

ER -