Finding and fixing faults. (English) Zbl 1159.68341
Borrione, Dominique (ed.) et al., Correct hardware design and verification methods. 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3–6, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29105-9/pbk). Lecture Notes in Computer Science 3725, 35-49 (2005).
Summary: We present a method for combined fault localization and correction for sequential systems. We assume that the specification is given in linear-time temporal logic and state the localization and correction problem as a game that is won if there is a correction that is valid for all possible inputs. For invariants, our method guarantees that a correction is found if one exists. The set of fault models we consider is very general: components can be replaced by arbitrary new functions. We compare our approach to model based diagnosis and show that it is more precise. We present experimental data that supports the applicability of our approach, obtained from a symbolic implementation of the algorithm in the Vis model checker.
For the entire collection see [Zbl 1089.68002].
For the entire collection see [Zbl 1089.68002].
MSC:
| 68M07 | Mathematical problems of computer architecture |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
