A Conservative Framework for Safety-Failure Checking

Frederic BEAL; Tomohiro YONEDA; Chris J. MYERS

doi:10.1093/ietisy/e91-d.3.642

A Conservative Framework for Safety-Failure Checking

Frederic BEAL, Tomohiro YONEDA, Chris J. MYERS

Full Text Views

0

Cite this

Summary :

We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.

Publication: IEICE TRANSACTIONS on Information Vol.E91-D No.3 pp.642-654

Publication Date: 2008/03/01

Publicized

Online ISSN: 1745-1361

DOI: 10.1093/ietisy/e91-d.3.642

Type of Manuscript: Special Section PAPER (Special Section on Test and Verification of VLSIs)

Category: Verification and Timing Analysis

Cite this

Copy

Frederic BEAL, Tomohiro YONEDA, Chris J. MYERS, "A Conservative Framework for Safety-Failure Checking" in IEICE TRANSACTIONS on Information, vol. E91-D, no. 3, pp. 642-654, March 2008, doi: 10.1093/ietisy/e91-d.3.642.
Abstract: We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.
URL: https://global.ieice.org/en_transactions/information/10.1093/ietisy/e91-d.3.642/_p

Copy

@ARTICLE{e91-d_3_642,
author={Frederic BEAL, Tomohiro YONEDA, Chris J. MYERS, },
journal={IEICE TRANSACTIONS on Information},
title={A Conservative Framework for Safety-Failure Checking},
year={2008},
volume={E91-D},
number={3},
pages={642-654},
abstract={We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.},
keywords={},
doi={10.1093/ietisy/e91-d.3.642},
ISSN={1745-1361},
month={March},}

Copy

TY - JOUR
TI - A Conservative Framework for Safety-Failure Checking
T2 - IEICE TRANSACTIONS on Information
SP - 642
EP - 654
AU - Frederic BEAL
AU - Tomohiro YONEDA
AU - Chris J. MYERS
PY - 2008
DO - 10.1093/ietisy/e91-d.3.642
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E91-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 2008
AB - We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.
ER -