TY - GEN
T1 - Partially Bounded Context-Aware Verification
AU - Le Roux, Luka
AU - Teodorov, Ciprian
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019/1/1
Y1 - 2019/1/1
N2 - Model-checking enables the formal verification of software systems. Powerful and automated, this technique suffers, however, from the state-space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. To address this problem, the Context-aware Verification (CaV) approach decomposes the verification problem using environment-based guides. This approach improves the scalability but it requires an acyclic specification of the verification guides, which are difficult to specify without losing completeness. In this paper, we present a new verification strategy that generalises CaV while ensuring the decomposability of the state-space. The approach relies on a language for the specification of the arbitrary guides, which relaxes the acyclicity requirement, and on a partially-bounded verification procedure. The effectiveness of our approach is showcased through a case-study from the aerospace domain, which shows that the scalability is maintained while easing the conception of the verification guides.
AB - Model-checking enables the formal verification of software systems. Powerful and automated, this technique suffers, however, from the state-space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. To address this problem, the Context-aware Verification (CaV) approach decomposes the verification problem using environment-based guides. This approach improves the scalability but it requires an acyclic specification of the verification guides, which are difficult to specify without losing completeness. In this paper, we present a new verification strategy that generalises CaV while ensuring the decomposability of the state-space. The approach relies on a language for the specification of the arbitrary guides, which relaxes the acyclicity requirement, and on a partially-bounded verification procedure. The effectiveness of our approach is showcased through a case-study from the aerospace domain, which shows that the scalability is maintained while easing the conception of the verification guides.
UR - https://www.scopus.com/pages/publications/85072871228
U2 - 10.1007/978-3-030-30446-1_28
DO - 10.1007/978-3-030-30446-1_28
M3 - Conference contribution
AN - SCOPUS:85072871228
SN - 9783030304454
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 532
EP - 548
BT - Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Proceedings
A2 - Ölveczky, Peter Csaba
A2 - Salaün, Gwen
PB - Springer Verlag
T2 - 17th International Conference on Software Engineering and Formal Methods, SEFM 2019
Y2 - 18 September 2019 through 20 September 2019
ER -