Efficient Verification of Software with Replicated Components

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

Concurrency is a model of computation that allows many units of executionto coexist. It is ubiquitous in computer science today: user processes in atime-sharing operating system execute concurrently, as do worker threads ina client-server environment. Parallel processing, once primarily ofinterest in high-performance computing, has emerged in recent years as anew way of increasing processing power, such as in multi-core concurrentsystems, even for the home personal computer.Concurrency poses new challenges for the quality assurance of software, fortwo reasons. First, concurrent programs have the potential for forms oferrors unknown in sequential computation, such as race conditions andmutual exclusion violations. Second, traditional reliability measures suchas simulation and testing fail in the presence of concurrency, due to thedifficulties of reproducing erroneous behavior. Model Checking is anautomated technique to reliably establish the correctness of software, orto reveal the existence of errors in a reproducible manner. A program isrepresented by a finite-state model, which is exhaustively searched forviolations of pre-specified properties.Exhaustive search, however, generally incurs a cost proportional to thenumber of model states that are reached during the search. This number isin turn worst-case exponential in the number of concurrent components. Thisstate space explosion problem has been a major obstacle to the widespreaduse of model checking.One avenue of our research is guided by the observation that concurrentsystems often consist of replicated components: instances of a singletemplate, generically describing the behavior of each component. Concurrentsystems of replicated components often exhibit a veryregular---symmetric---structure: their behavior is invariant underinterchanges of the components. This causes redundancy in the system modeland in the (naive) exploration of the model's state space.We propose to investigate the efficacy of symmetry reduction andparameterized verification to attack the state space explosion problem forsoftware with replicated components. Both techniques have shown to betremendously effective in principle, namely due to their potential ofreducing the size of a symmetric system by an exponential factor, or ofcollapsing the verification problem for an infinite family of systems toone for a single system or a small finite family, respectively.The applicability of these techniques to concurrent software was hampered,however, by the apparent incapability of model checking to deal withinteger variables over very large domains or even unbounded, dynamic datastructures. The situation changed dramatically with the advent of automatedabstraction-refinement techniques. Software is initially representedabstractly using coarse finite-state models, risking the possibility ofincorrect---spurious---verification results. The new paradigm came withways of detecting spuriousness, and of dealing with it by iterativelyrefining the abstract model until spurious behavior is removed.To sum up, concurrent software exhibits two sources of complexity: largevariable data domains and concurrency. Fortunately, these sources areorthogonal and can be attacked separately. This separation makes itpossible to apply symmetry reduction and parameterized techniques toconcurrent software, methods that target the concurrency aspect of statespace explosion. The ultimate goal of the proposed work is to combine thesemethods with iterative abstraction refinement to obtain verification toolsfor concurrent software that can seriously curb state space explosion atall levels.

Publications

10 25 50
publication icon
Basler G (2010) Context-aware counter abstraction in Formal Methods in System Design

publication icon
Blanc N (2010) Race analysis for systemc using model checking in ACM Transactions on Design Automation of Electronic Systems

publication icon
Brillout A (2011) An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic in Journal of Automated Reasoning

publication icon
Chockler H (2012) Computing Mutation Coverage in Interpolation-Based Model Checking in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

publication icon
Cook B (2013) Ranking function synthesis for bit-vector relations in Formal Methods in System Design

publication icon
D'Silva V (2012) Static Analysis

publication icon
Donaldson A (2012) Counterexample-guided abstraction refinement for symmetric concurrent programs in Formal Methods in System Design

publication icon
Donaldson A (2011) Automatic analysis of DMA races using model checking and k-induction in Formal Methods in System Design

 
Description There exists an extensive range of applications for CBMC, the software tool developed by this grant, for full details see http://www.cprover.org/cbmc/applications.shtml. CBMC has been used in the automotive industry for checking functionality of software, for verification of C code in pacemakers, for analysing driver interactions with semi-autonomous vehicles, and for runtime verification in ultra-critical systems used in aircraft.
First Year Of Impact 2010
Sector Digital/Communication/Information Technologies (including Software),Electronics,Energy,Healthcare,Manufacturing, including Industrial Biotechology,Security and Diplomacy,Transport
Impact Types Economic

 
Description European Research Council
Amount £1,098,069 (GBP)
Funding ID CPROVER 
Organisation European Research Council (ERC) 
Sector Public
Country Belgium
Start 10/2011 
End 11/2016