Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing

Reference:

Jori Dubrovin. Checking bounded reachability in asynchronous systems by symbolic event tracing. In Gilles Barthe and Manuel Hermenegildo, editors, Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2010), volume 5944 of Lecture Notes in Computer Science, pages 146–162. Springer, 2010.

Abstract:

This paper presents a new framework for checking bounded reachability properties of asynchronous systems by reducing the problem to satisfiability in difference logic. The analysis is bounded by fixing a finite set of potential events, each of which may occur at most once in any order. The events are specified using high-level Petri nets. The proposed logic encoding describes the space of possible causal links between events rather than possible sequences of states as in Bounded Model Checking. Independence between events is exploited intrinsically without partial order reductions, and the handling of data is symbolic. Experiments with a proof-of-concept implementation of the technique show that it has the potential to far exceed the performance of Bounded Model Checking.

Keywords:

formal verification, Bounded Model Checking, partial order method, Coloured Petri Nets, difference logic

Suggested BibTeX entry:

@inproceedings{Dub:VMCAI10,
    author = {Jori Dubrovin},
    booktitle = {Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2010)},
    editor = {Gilles Barthe and Manuel Hermenegildo},
    pages = {146--162},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing},
    volume = {5944},
    year = {2010},
}