Sciweavers

Share
TPHOL
2008
IEEE

Formal Reasoning About Causality Analysis

8 years 9 months ago
Formal Reasoning About Causality Analysis
Systems that can immediately react to their inputs may suffer from cyclic dependencies between their actions and the corresponding trigger conditions. For this reason, causality analysis has to be employed to check the constructiveness of the programs which implies the existence of unique and consistent behaviours. In this paper, we describe the embedding of various views of causality analysis into the HOL4 theorem prover to check their equivalence. In particular, we show the equivalence between the classical analysis procedure, which is based on a fixpoint computation, and a formulation as a (bounded) model checking problem.
Jens Brandt, Klaus Schneider
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Jens Brandt, Klaus Schneider
Comments (0)
books