Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
TY - GEN
T1 - Supporting domain-specific state space reductions through local partial-order reduction
AU - Bokor, P.
AU - Kinder, J.
AU - Serafini, M.
AU - Suri, Neeraj
PY - 2011/11/6
Y1 - 2011/11/6
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. © 2011 IEEE.
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. © 2011 IEEE.
KW - Concurrent software systems
KW - Domain specific
KW - Execution paths
KW - Java PathFinder
KW - Liveness properties
KW - Long-path
KW - Message passing systems
KW - Model checker
KW - Partial-order reduction
KW - Single state
KW - State-space explosion
KW - State-space reduction
KW - Stubborn sets
KW - Message passing
KW - Software engineering
KW - Model checking
U2 - 10.1109/ASE.2011.6100044
DO - 10.1109/ASE.2011.6100044
M3 - Conference contribution/Paper
SN - 9781457716386
SP - 113
EP - 122
BT - 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)
PB - IEEE
ER -