Partially Bounded Context-Aware Verification

Luka Le Roux (1) , Ciprian Teodorov (1)

1 Lab-STICC_ENSTAB_ CACS_MOCS

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.

Mots clés: Model checking

Domaines: Sciences de l'ingénieur [physics]; Génie logiciel [cs.SE]

Luka Le Roux, Ciprian Teodorov. Partially Bounded Context-Aware Verification. 17th International Conference on Software Engineering and Formal Methods, SEFM 2019, Sep 2019, Oslo, Norway. pp.532-548, ⟨10.1007/978-3-030-30446-1_28⟩. ⟨hal-02434620⟩