N. Timm:

**Three-Valued Abstraction and Heuristic-Guided Refinement for Verifying Concurrent Systems**. PhD thesis, University of Paderborn (2013)

[

Show Abstract]

Software systems are playing an increasing role in our everyday life, and as

the amount of software applications grows, so does their complexity and the

relevance of their computations. Software components can be found in many

systems that are charged with safety-critical tasks, such as control systems

for aviation or power plants. Hence, software verification techniques that are

capable of proving the absence of critical errors are becoming more and more

important in the field software engineering.

A well-established approach to software verification is model checking.

Applying this technique involves an exhaustive exploration of a state space

model corresponding to the system under consideration. The major challenge

in model checking is the so-called state explosion problem: The state space of a

software system grows exponentially with its size. Thus, the straightforward

modelling of real-life systems practically impossible. A common approach to

this problem is the application of abstraction techniques, which reduce the

original state space by mapping it on a significantly smaller abstract one.

Abstraction inherently involves a loss of information, and thus, the resulting

abstract model may be too imprecise for a definite result in verification.

Therefore, abstraction is typically combined with abstraction refinement: An

initially very coarse abstract model is iteratively refined, i.e. enriched with

new details about the original system, until a level of abstraction is reached

that is precise enough for a definite outcome. Abstraction refinement-based

model checking is fully automatable and it is considered as one of the most

promising approaches to the state explosion problem in verification. However,

it is still faced with a number of challenges. There exist several types of

abstraction techniques and not every type is equally well-suited for all kinds of

systems and verification tasks. Moreover, the selection of adequate refinement

steps is nontrivial and typically the most crucial part of the overall approach:

Unfavourable refinement decisions can compromise the state space-reducing

effect of abstraction, and as a consequence, can easily lead to the failure

of verification. It is, however, hard to predict which refinement steps will

eventually be expedient for verification – and which not. In this thesis, we approach the previously addressed challenges of abstraction

refinement-based model checking by focusing on one specific type

of software system: Concurrent systems are compositions of interleaved executed

software processes that communicate via shared variables or message

passing, which makes their verification particularly difficult. However, these

systems also reveal a high amount of structural information – in particular, the

communication dependencies between processes – that we exploit for improving

abstraction and refinement. To this end, we introduce a comprehensive

verification framework for concurrent systems.

Our approach to abstraction is based on a combination of predicate abstraction

– a data abstraction technique that replaces concrete system variables by

predicates – and spotlight abstraction – a technique that abstracts away entire

processes of a concurrent system. We thus tackle the two major causes of state

explosion for concurrent systems. Another key feature of our approach is the

use of a three-valued abstract domain. Properties in our models can take the

values true, false and unknown, which enables us to explicitly model the loss

of information due to abstraction: All true and false results obtained via model

checking can be transferred to the original system, only an unknown outcome necessitates abstraction refinement.

For automatically refining the abstract models we follow the concept of

counterexample-guided abstraction refinement (CEGAR). Counterexamples are

’unknown’ error paths in the abstract model that typically hint at several possible

ways to resolve the uncertainty via refinement. In our scenario, these

refinement steps can involve the addition of new predicates or new processes.

However, not every potential refinement step is expedient, which makes the

selection of an appropriate step an exceedingly difficult task. Therefore, we

introduce a variant of CEGAR enhanced by heuristic guidance: Based on an

iterative abstraction dependence analysis the possible refinement steps are

heuristically evaluated with regard to their benefit for the current verification

task, and the best evaluated step is chosen for refinement. In two case

studies, we demonstrate that our heuristic approach can significantly improve

the performance of abstraction-refinement-based verification of concurrent

systems. Our developed verification framework primarily allows for reasoning about

safety and liveness properties of concurrent systems that are composed of a

fixed number of processes. However, we also introduce an extension that facilitates

the verification of parameterised systems – compositions of an unbounded

number of homogeneous processes. Our extension is based on a combination

spotlight abstraction with symmetry reduction, a reduction technique that

exploits the homogeneity in parameterised systems.

[

PDF] [

Show BibTeX]

@phdthesis{NT2013,

author = {N. Timm},

title = {Three-Valued Abstraction and Heuristic-Guided Refinement for Verifying Concurrent Systems},

year = {2013},

year = {2013},

school = {University of Paderborn}

}

N. Timm, H. Wehrheim, M. Czech:

**Heuristic-Guided Abstraction Refinement for Concurrent Systems**. In T. Aoki and K. Tagushi (eds.): Proceedings of the 14th International Conference on Formal Engineering Methods and Software Engineering ICFEM'12. Springer Berlin/Heidelberg, pp. 348-363 (2012)

[

Show Abstract]

Predicate abstraction is an established technique in software verification. It inherently includes an abstraction refinement loop successively adding predicates until the right level of abstraction is found. For concurrent systems, predicate abstraction can be combined with spotlight abstraction, further reducing the state space by abstracting away certain processes. Refinement then has to decide whether to add a new predicate or a new process. Selecting the right predicates and processes is a crucial task: The positive effect of abstraction may be compromised by unfavourable refinement decisions. Here we present a heuristic approach to abstraction refinement. The basis for a decision is a set of refinement candidates, derived by multiple counterexample-generation. Candidates are evaluated with respect to their influence on other components in the system. Experimental results show that our technique can significantly speed up verification as compared to a naive abstraction refinement.

[

Show BibTeX]

@inproceedings{TWC2012,

author = {N. Timm AND H. Wehrheim AND M. Czech},

title = {Heuristic-Guided Abstraction Refinement for Concurrent Systems},

editor = {T. Aoki and K. Tagushi},

booktitle = {Proceedings of the 14th International Conference on Formal Engineering Methods and Software Engineering ICFEM'12},

journal = {LNCS 7635},

year = {2012},

pages = {348-363},

publisher = {Springer Berlin/Heidelberg},

year = {2012}

}

N. Timm, H. Wehrheim:

**On Symmetries and Spotlights - Verifying Parameterised Systems**. In J.S. Dong, H.Zhu (eds.): Proceedings of the 12th International Conference on Formal Engineering Methods and Software Engineering ICFEM'10. Springer Verlag Berlin-Heidelberg, LNCS, vol. 6447, pp. 534-548 (2010)

[

Show Abstract]

Parameterised model checking is concerned with verifying properties of

arbitrary numbers of homogeneous processes composed in parallel. The

problem is known to be undecidable in general. Nevertheless, a number

of approaches have developed verification techniques for certain

classes of parameterised systems. Here, we present an approach combining symmetry arguments with spotlight

abstractions. The technique determines (the size of) a particular instantiation of the parameterised system from the given temporal

logic formula, and feds this into an abstracting model checker. The

degree of abstraction with respect to processes occurring during model

checking determines whether the obtained result is also valid for all other instantiations. This enables us to prove safety as well as liveness properties (specified in full CTL) of parameterised systems on very small instantiations.

[

PDF] [

Show BibTeX]

@inproceedings{TW10,

author = {N. Timm AND H. Wehrheim},

title = {On Symmetries and Spotlights - Verifying Parameterised Systems},

editor = {J.S. Dong, H.Zhu},

booktitle = {Proceedings of the 12th International Conference on Formal Engineering Methods and Software Engineering ICFEM'10},

year = {2010},

volume = {6447},

pages = {534-548},

publisher = {Springer Verlag Berlin-Heidelberg},

year = {2010}

}

N. Timm:

**A Bounded Model Checker for Partially Known Systems**. In

*Proceedings of the 21st Nordic Workshop on Programming Theory. Technical University of Denmark*, pp. 17-19. (2009)

[

Show BibTeX]

@article{timm2009bounded,

author = {N. Timm},

title = {A Bounded Model Checker for Partially Known Systems},

journal = {Proceedings of the 21st Nordic Workshop on Programming Theory. Technical University of Denmark},

year = {2009},

pages = {17-19},

year = {2009}

}

N. Timm:

**Bounded Model Checking für partielle Systeme**. Master's thesis, University of Paderborn (2009)

[

PDF] [

Show BibTeX]

@mastersthesis{NTMT2009,

author = {N. Timm},

title = {Bounded Model Checking f{\"u}r partielle Systeme},

year = {2009},

year = {2009},

school = {University of Paderborn}

}

N. Timm:

**CSI: PC2 - A High Performance Biometric System**. In Informatiktage 2008: Fachwissenschaftlicher Informatik-Kongress. , Lecture Notes in Informatics, vol. S-6, pp. 209-212 (2008)

[

Show BibTeX]

@inproceedings{NT2008,

author = {N. Timm},

title = {CSI: PC2 - A High Performance Biometric System},

booktitle = {Informatiktage 2008: Fachwissenschaftlicher Informatik-Kongress},

year = {2008},

volume = {S-6},

pages = {209--212},

year = {2008}

}