Checking bounded reachability in asynchronous systems by symbolic event tracing
No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Faculty of Information and Natural Sciences |
D4 Julkaistu kehittämis- tai tutkimusraportti taikka -selvitys
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Author
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
