2011 IEEE 13th International Symposium on High-Assurance Systems Engineering (2011)
Boca Raton, Florida USA
Nov. 10, 2011 to Nov. 12, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/HASE.2011.15
Partial order reduction is essential to address state explosion when verifying concurrent systems by reducing states irrelevant to the verification results. However, traditional static approaches by analyzing system model structures often do not work well. To address such problem, this paper presents a new behavioral analysis approach where a compositional reach ability analysis method is used to generate the over-approximate state spaces for all modules in a system, and then the independent transitions necessary for the partial order reduction are computed by examining these state spaces. Compared to the static analysis approaches, the independent transitions computed are more refined and accurate. The experimental results on some examples show that the presented approach is promising.
model checking, labeled petri-nets, partial order reduction, behavioral analysis, compositional verification
C. Myers, Y. Zhang, E. Rodriguez and H. Zheng, "A Behavioral Analysis Approach for Efficient Partial Order Reduction," 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering(HASE), Boca Raton, Florida USA, 2011, pp. 49-56.