Formal verification of mutual exclusion between the guards of deterministic choice structures

M. Boubekeur; K. L. Man; M. P. Schellekens

doi:10.1109/CCECE.2007.356

Formal verification of mutual exclusion between the guards of deterministic choice structures

M. Boubekeur^*, K. L. Man, M. P. Schellekens

^*Corresponding author for this work

University College Cork

Research output: Chapter in Book or Report/Conference proceeding › Conference Proceeding › peer-review

Abstract

The formal verification of mutual exclusion between the guards of a deterministic choice structure is of great interest to the asynchronous circuit designers. To perform this spot of checking, we propose a treatment in two phases; the first is based on a static analysis, the Mutual Exclusion (ME) is checked using a symbolic decision tool. In the second phase, if the static analysis returns a result like "the model does not satisfy mutual exclusion", the dynamic verification takes into account the constraints of the environment to refine the analysis. If the mutual exclusion is still not satisfied, it gives a counter-example. The principle is to check wether indeterminism exists during the construction of the whole execution model, using a model-checking tool.

Original language	English
Title of host publication	2007 Canadian Conference on Electrical and Computer Engineering, CCECD
Pages	1417-1420
Number of pages	4
DOIs	https://doi.org/10.1109/CCECE.2007.356
Publication status	Published - 2007
Externally published	Yes
Event	2007 Canadian Conference on Electrical and Computer Engineering, CCECD - Vancouver, BC, Canada Duration: 22 Apr 2007 → 26 Apr 2007

Publication series

Name	Canadian Conference on Electrical and Computer Engineering
ISSN (Print)	0840-7789

Conference

Conference	2007 Canadian Conference on Electrical and Computer Engineering, CCECD
Country/Territory	Canada
City	Vancouver, BC
Period	22/04/07 → 26/04/07

Access to Document

10.1109/CCECE.2007.356

Cite this

@inproceedings{c30f00182bd9413bbb2da03d4058632e,

title = "Formal verification of mutual exclusion between the guards of deterministic choice structures",

abstract = "The formal verification of mutual exclusion between the guards of a deterministic choice structure is of great interest to the asynchronous circuit designers. To perform this spot of checking, we propose a treatment in two phases; the first is based on a static analysis, the Mutual Exclusion (ME) is checked using a symbolic decision tool. In the second phase, if the static analysis returns a result like {"}the model does not satisfy mutual exclusion{"}, the dynamic verification takes into account the constraints of the environment to refine the analysis. If the mutual exclusion is still not satisfied, it gives a counter-example. The principle is to check wether indeterminism exists during the construction of the whole execution model, using a model-checking tool.",

author = "M. Boubekeur and Man, {K. L.} and Schellekens, {M. P.}",

year = "2007",

doi = "10.1109/CCECE.2007.356",

language = "English",

isbn = "1424410215",

series = "Canadian Conference on Electrical and Computer Engineering",

pages = "1417--1420",

booktitle = "2007 Canadian Conference on Electrical and Computer Engineering, CCECD",

note = "2007 Canadian Conference on Electrical and Computer Engineering, CCECD ; Conference date: 22-04-2007 Through 26-04-2007",

}

Boubekeur, M, Man, KL & Schellekens, MP 2007, Formal verification of mutual exclusion between the guards of deterministic choice structures. in 2007 Canadian Conference on Electrical and Computer Engineering, CCECD., 4233015, Canadian Conference on Electrical and Computer Engineering, pp. 1417-1420, 2007 Canadian Conference on Electrical and Computer Engineering, CCECD, Vancouver, BC, Canada, 22/04/07. https://doi.org/10.1109/CCECE.2007.356

Formal verification of mutual exclusion between the guards of deterministic choice structures. / Boubekeur, M.; Man, K. L.; Schellekens, M. P.
2007 Canadian Conference on Electrical and Computer Engineering, CCECD. 2007. p. 1417-1420 4233015 (Canadian Conference on Electrical and Computer Engineering).

Research output: Chapter in Book or Report/Conference proceeding › Conference Proceeding › peer-review

TY - GEN

T1 - Formal verification of mutual exclusion between the guards of deterministic choice structures

AU - Boubekeur, M.

AU - Man, K. L.

AU - Schellekens, M. P.

PY - 2007

Y1 - 2007

N2 - The formal verification of mutual exclusion between the guards of a deterministic choice structure is of great interest to the asynchronous circuit designers. To perform this spot of checking, we propose a treatment in two phases; the first is based on a static analysis, the Mutual Exclusion (ME) is checked using a symbolic decision tool. In the second phase, if the static analysis returns a result like "the model does not satisfy mutual exclusion", the dynamic verification takes into account the constraints of the environment to refine the analysis. If the mutual exclusion is still not satisfied, it gives a counter-example. The principle is to check wether indeterminism exists during the construction of the whole execution model, using a model-checking tool.

AB - The formal verification of mutual exclusion between the guards of a deterministic choice structure is of great interest to the asynchronous circuit designers. To perform this spot of checking, we propose a treatment in two phases; the first is based on a static analysis, the Mutual Exclusion (ME) is checked using a symbolic decision tool. In the second phase, if the static analysis returns a result like "the model does not satisfy mutual exclusion", the dynamic verification takes into account the constraints of the environment to refine the analysis. If the mutual exclusion is still not satisfied, it gives a counter-example. The principle is to check wether indeterminism exists during the construction of the whole execution model, using a model-checking tool.

UR - http://www.scopus.com/inward/record.url?scp=48749110021&partnerID=8YFLogxK

U2 - 10.1109/CCECE.2007.356

DO - 10.1109/CCECE.2007.356

M3 - Conference Proceeding

AN - SCOPUS:48749110021

SN - 1424410215

SN - 9781424410217

T3 - Canadian Conference on Electrical and Computer Engineering

SP - 1417

EP - 1420

BT - 2007 Canadian Conference on Electrical and Computer Engineering, CCECD

T2 - 2007 Canadian Conference on Electrical and Computer Engineering, CCECD

Y2 - 22 April 2007 through 26 April 2007

ER -

Formal verification of mutual exclusion between the guards of deterministic choice structures

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this