TY - GEN
T1 - Formal verification of infinite-state BIP models
AU - Bliudze, Simon
AU - Cimatti, Alessandro
AU - Jaber, Mohamad
AU - Mover, Sergio
AU - Roveri, Marco
AU - Saab, Wajeb
AU - Wang, Qiang
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015/1/1
Y1 - 2015/1/1
N2 - We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose considerable restrictions: they either verify finite-state systems or they do not handle the transfer of data on the interactions and priorities. Firstly, we propose an instantiation of the ESST (Explicit Scheduler Symbolic Thread) framework to verify BIP models. The key insight is to apply symbolic reasoning to analyze the behavior of the system described by the BIP components, and an explicit-state search to analyze the behavior of the system induced by the BIP interactions and priorities. The combination of symbolic and explicit exploration techniques allow to benefit from abstraction, useful when reasoning about data, and from partial order reduction, useful to mitigate the state space explosion due to concurrency. Secondly, we propose an encoding from a BIP model into a symbolic, infinite-state transition system. This technique allows us to leverage the state of the art verification algorithms for the analysis of infinite-state systems. We implemented both techniques and we evaluated their performance against the existing approaches. The results show the effectiveness of our approaches with respect to the state of the art, and their complementarity for the analysis of safe and unsafe BIP models.
AB - We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose considerable restrictions: they either verify finite-state systems or they do not handle the transfer of data on the interactions and priorities. Firstly, we propose an instantiation of the ESST (Explicit Scheduler Symbolic Thread) framework to verify BIP models. The key insight is to apply symbolic reasoning to analyze the behavior of the system described by the BIP components, and an explicit-state search to analyze the behavior of the system induced by the BIP interactions and priorities. The combination of symbolic and explicit exploration techniques allow to benefit from abstraction, useful when reasoning about data, and from partial order reduction, useful to mitigate the state space explosion due to concurrency. Secondly, we propose an encoding from a BIP model into a symbolic, infinite-state transition system. This technique allows us to leverage the state of the art verification algorithms for the analysis of infinite-state systems. We implemented both techniques and we evaluated their performance against the existing approaches. The results show the effectiveness of our approaches with respect to the state of the art, and their complementarity for the analysis of safe and unsafe BIP models.
U2 - 10.1007/978-3-319-24953-7_25
DO - 10.1007/978-3-319-24953-7_25
M3 - Conference contribution
AN - SCOPUS:84951762972
SN - 9783319249520
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 326
EP - 343
BT - Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Proceedings
A2 - Finkbeiner, Bernd
A2 - Pu, Geguang
A2 - Zhang, Lijun
PB - Springer Verlag
T2 - 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
Y2 - 12 October 2015 through 15 October 2015
ER -