Checking bounded reachability in asynchronous systems by symbolic event tracing

No Thumbnail Available

URL

Journal Title

Journal ISSN

Volume Title

Faculty of Information and Natural Sciences | D4 Julkaistu kehittämis- tai tutkimusraportti taikka -selvitys

Date

2009

Major/Subject

Mcode

Degree programme

Language

en

Pages

33

Series

TKK reports in information and computer science, 14

Abstract

This report presents a new symbolic technique for checking reachability properties of asynchronous systems by reducing the problem to satisfiability in restrained 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 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. On a family of benchmarks, the proposed approach is consistently faster than Bounded Model Checking. In addition, this report presents a compact encoding of the restrained subset of difference logic in propositional logic.

Description

Keywords

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

Other note

Citation

Permanent link to this item

https://urn.fi/urn:nbn:fi:tkk-012995