The aim of the FME3 project is to develop and evaluate a new methodology for
analyzing the robustness of circuits described at the RT level, with respect
to errors caused by transient faults.
We propose to improve efficiency and accuracy by combining fault injection
techniques and formal methods. The keystone of our approach will be a functional
modeling of both the device and the fault models. Such a formalization will fit
the capabilities of model checking tools as well as of theorem provers, thus
giving the possibility to consider various kinds of circuit descriptions,
including parameterized ones.
The overall structure of the project is as follows. Starting from a RTL description,
a technique based on symbolic simulation will produce a functional representation
M of the transition and output functions (we will extend and
reimplement a methodology developed in the TIMA-VDS team). Fault injection will also
be functionaly or logically formalized, and combining it with M will yield a model M' of faulty
system. Then two issues will be
considered:
the verification of logico-temporal properties for M', e.g. "the detection
signal is always asserted when an erroneous configuration occurs", expressed in a
specification language like PSL.
the evaluation of the safety or security level.
The goal here is to analyze on the reachable state space the ability of the circuit
to avoid unacceptable failures. In the case where error detection (or correction)
logic exists, it would also be possible to analyze its capability to handle the
injected faults.
Based on these principles, and as explained in our paper of DFT'2009 (see below), we are currently
(end of 2009) developing complementary formal approaches for robustness analysis.
Combining approaches based on theorem proving and on model checking can lead to a
comprehensive robustness evaluation methodology. In a first step, deductive proofs
(efficient at abstract levels, and also on parameterized systems)
can determine robustness properties, in particular is the circuit robust or not, using
a meta-model for representing faults. Then,
if it is not robust, the computation of the ratios of either potentially or
systematically repairing states may give some indications about the robustness of
the circuit and may guide the search of the minimal subset of registers to be
protected in order to achieve the required robustness
if it is robust, the computation of the length of repairing sequences may characterize the
repairing speed of the circuit. This measure may be used to find an alternative architecture
with a better repairing speed.
Slides: LTL model checking and some optimizations (MC-SOG)
Slides: Symmetry reduction for temporal model checking
Slides: Impacts de transformations d'un système
sur sa spécification et sa vérification
Participation au Colloque National du GDR SoC-SiP,
Juin 2008. Présentation du poster "Premiers résultats sur l'utilisation d'ACL2 pour
l'évaluation de la conséquence des erreurs logiques"
(papier)
Technical meetings: June 6, 2008 (Paris) and July 4, 2008 (Grenoble)
Task 2: symbolic simulator
Task 3: first results with ACL2 and with model checkers
Technical meeting: October 13, 2008 (Paris)
Task 2: last improvements of the symbolic simulator
Task 3: new results with model checkers and constraints solvers
Task 3: new results with ACL2 (hierarchical proofs)
Technical meeting: February 27, 2009 (Grenoble)
Tasks 3 and 4: formal reasoning with ACL2, for hierarchical and parameterized architectures
Tasks 5 and 6: using model checkers and constraints solvers for evaluating the robustness level
Dissemination of results
Participation to the IEEE Workshop on Silicon Errors in Logic - System Effects
(SELSE), Stanford University (CA), March 2009.
Presentation of the paper entitled "Soft Error Effect and Register Criticality
Evaluations: Past, Present and Future" (paper)
Technical meeting: July 8, 2009 (Paris)
Tasks 5 and 6: using model checkers for evaluating the robustness level, improvement of the
"repairing" model
Organisational issues
Project review: September 10, 2009
Technical meeting: November 13, 2009 (Paris)
Tasks 3 and 4: new (higher order) fault model for a deduction-oriented reasoning about hierarchical and
parameterized architectures, first implementation in PVS
Participation au Grand Colloque STIC, Paris,
Janvier 2010 (présentation d'un poster)
Technical meeting: March 26, 2010 (Grenoble)
Tasks 3 and 4: last improvements for the new (higher order) fault model and its implementation in PVS
Tasks 5 and 6: last improvements for the definitions of classes of robustness and their implementations
in model-checkers and in theorem provers
Discussion on component replacement in formal models
Technical meeting: November 5, 2010 (Paris)
Publications - Outcomes
R.Leveugle, L.Pierre, P.Maistri, R.Clavel: "Soft Error Effect and Register Criticality Evaluations:
Past, Present and Future". Proc. IEEE Workshop on Silicon Errors in Logic - System Effects,
Stanford University (CA), March 2009.
F.Ouchet, D.Borrione, K.Morin-Allory, L.Pierre: "High-level symbolic simulation
for automatic model extraction". Proc. IEEE Symposium on Design and Diagnostics of
Electronic Systems, Liberec (Czech Republic), April 2009.
IEEE page
VSYML:
VHDL symbolic simulator (outcome of Task 2)
L.Pierre, R.Clavel, R.Leveugle: "ACL2 for the Verification of Fault-Tolerance
Properties: First Results". Proc. International Workshop On The ACL2 Theorem Prover
and Its Applications, Boston (MA), May 2009.
ACM page,
ACL2 books
S.Baarir, C.Braunstein, R.Clavel, E.Encrenaz, J.M.Ilié, R.Leveugle, I.Mounier,
L.Pierre, D.Poitrenaud : "Complementary Formal Approaches for Dependability Analysis".
Proc. IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT'09),
Chicago (IL), October 2009.
IEEE page
S.Baarir, C.Braunstein, E.Encrenaz, J.M.Ilié, T.Li, I.Mounier, D.Poitrenaud, S.Younes :
"Quantifying Robustness by Symbolic Model checking".
Proc. Hardware Verification Workshop 2010, Edinburgh (UK), July 2010.
R.Leveugle: "Early Robustness Evaluation of Digital Integrated Systems". Tutorial "Robustness" at
FDL'2010 (Forum for Design Languages), Southampton (UK), September 2010.
S.Baarir, C.Braunstein, E.Encrenaz, J.M.Ilié, T.Li, I.Mounier, D.Poitrenaud, S.Younes :
"Feasibility Analysis for Robustness Quantification by Symbolic Model checking".
Formal Methods in System Design (Springer), 2011.
Back to the VDS Home Page
