Performing causality analysis by bounded model checking

13 years 4 months ago
Performing causality analysis by bounded model checking
Synchronous systems can immediately react to the inputs of their environment which may lead to so-called causality cycles between actions and their trigger conditions. Systems with causality cycles may not be consistent or may become nondeterministic. For this reason, compilers for synchronous languages usually employ special analyses to guarantee a predictable runtime behavior of the considered programs. In this paper, we show how causality analysis can be formulated as a model checking problem, so that all of the sophisticated algorithms originally developed for model checking can now also be used for causality analysis. To this end, we model the ‘micro step’ behavior of synchronous programs in terms of a transition relation that can be directly used for symbolic model checking. Moreover, we show that the obtained model checking problems can be even decided by bounded model-checking problems so that modern SAT-solvers can be used to efficiently solve the causality problem.
Klaus Schneider, Jens Brandt
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2008
Where ACSD
Authors Klaus Schneider, Jens Brandt
Comments (0)