A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
Authors:
- 1 November 2008
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 1-9
Abstract
The quality of formal specifications and the circuits they are written for can be evaluated through checks such as vacuity and coverage. Both checks involve mutations to the specification or the circuit implementation. In this context, we study and prove properties of mutations to finite-state systems. Since faults can be viewed as mutations, our theory of mutations can also be used in a formal approach to fault injection. We demonstrate theoretically and with experimental results how relations and orders amongst mutations can be used to improve specifications and reason about coverage of fault tolerant circuits.Keywords
This publication has 6 references indexed in Scilit:
- What causes a system to satisfy a specification?ACM Transactions on Computational Logic, 2008
- Branching vs. Linear Time: Semantical Perspective2007
- Verification-Guided Soft Error Resilience2007
- Vacuity detection in temporal model checkingInternational Journal on Software Tools for Technology Transfer, 2003
- Model checking and modular verificationACM Transactions on Programming Languages and Systems, 1994
- Characterizing finite Kripke structures in propositional temporal logicTheoretical Computer Science, 1988