Past‐Free[ze] reachability analysis: reaching further with DAG‐directed exhaustive state‐space analysis. (31st August 2016)

• Record Type: Journal Article
• Authors: Teodorov, Ciprian; Le Roux, Luka; Drey, Zoé; Dhaussy, Philippe
• Is Part Of: Software testing, verification & reliability. Volume 26:Number 7(2016)
• Page Start: 516
• Page End: 542
• Publication Date: 2016-08-31
• Subjects: reachability analysis -- formal verification -- context‐aware verification -- directed‐acyclic graph -- semi‐external algorithms; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1611
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: Model‐checking enables the automated formal verification of software systems through the explicit enumeration of all the reachable states. While this technique has been successfully applied to industrial systems, it suffers from the state‐space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. In this paper, we present a new reachability analysis algorithm, named Past‐Free[ze], that reduces the state‐space explosion problem by freeing parts of the state‐space from memory. This algorithm relies on the explicit isolation of the acyclic parts of the system before analysis. The parallel composition of these parts drives the reachability analysis, the core of all model‐checkers. During the execution, the past states of the system are freed from memory making room for more future states. To enable counter‐example construction, the past states can be stored on external storage. To show the effectiveness of the approach, the algorithm was implemented in the OBP Observation Engine and was evaluated both on a synthetic benchmark and on realistic case studies from automotive and aerospace domains. The benchmark, composed of 50 test cases, shows that in average, 75 % of the state‐space can be dropped from memory thus enabling the exploration of up to 14 times more states than traditional approaches. Moreover, in some cases, the reachability analysis time can be reduced by up to 25 % . In realistic settings, the use of Past‐Free[ze] enabled the exploration of a state‐space 4.5 times larger on the automotive case study, where almost 50 % of the states are freed from memory. Moreover, this approach offers the possibility of analyzing an arbitrary number of interactions between the environment and the system‐under‐verification; for instance, in the case of the aerospace example, 1000 pilot/system interactions could be analyzed unraveling an 80 GB state‐space using only 10 GB of memory. Copyright © 2016 John Wiley & Sons, Ltd. Abstract : This paper presents Past‐Free[ze], a new reachability algorithm that reduces the state‐space explosion problem during model‐checking. This algorithm relies on the explicit isolation of the acyclic parts of the system, which are used as a guide for freeing the past states of the system, making room for more future states. The algorithm effectiveness was evaluated both on a synthetic benchmark and on realistic case studies. The results show that up to 75% of the state‐space can be dropped from memory