The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
A verificação de modelo CTL (Computation Tree Logic) é um método formal de verificação de projeto que verifica se o comportamento do sistema verificado está contido no da especificação de requisitos. Se esta verificação não for aprovada, o verificador de modelo CTL gera um subconjunto de estados justos que pertence ao sistema, mas não à especificação. Nesta carta, apresentamos um método incremental que modifica sucessivamente o último resultado da verificação cada vez que o projeto é modificado. Nosso algoritmo incremental permite que o designer faça alterações em termos de adição ou subtração de fórmulas CTL justas ou restrições de justiça no comportamento aceitável da declaração do problema. Em seguida, essas alterações são adotadas para atualizar o conjunto de estados justos calculado anteriormente. Nosso algoritmo incremental mostra-se melhor do que as técnicas não incrementais atuais para verificação de modelo CTL. Além disso, uma conclusão apoiada pelos resultados experimentais é apresentada aqui.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copiar
Victor R. L. SHEN, "Incremental CTL Model Checker for Fair States" in IEICE TRANSACTIONS on Information,
vol. E82-D, no. 7, pp. 1126-1130, July 1999, doi: .
Abstract: CTL (Computation Tree Logic) model checking is a formal method for design verification that checks whether the behavior of the verified system is contained in that of the requirements specification. If this check doesn't pass, the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incremental method which successively modifies the latest verification result each time the design is modified. Our incremental algorithm allows the designer to make changes in terms of addition or subtraction of fair CTL formulas, or fairness constraints on acceptable behavior from the problem statement. Then, these changes are adopted to update the set of fair states computed earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusion supported by the experimental results is presented herein.
URL: https://global.ieice.org/en_transactions/information/10.1587/e82-d_7_1126/_p
Copiar
@ARTICLE{e82-d_7_1126,
author={Victor R. L. SHEN, },
journal={IEICE TRANSACTIONS on Information},
title={Incremental CTL Model Checker for Fair States},
year={1999},
volume={E82-D},
number={7},
pages={1126-1130},
abstract={CTL (Computation Tree Logic) model checking is a formal method for design verification that checks whether the behavior of the verified system is contained in that of the requirements specification. If this check doesn't pass, the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incremental method which successively modifies the latest verification result each time the design is modified. Our incremental algorithm allows the designer to make changes in terms of addition or subtraction of fair CTL formulas, or fairness constraints on acceptable behavior from the problem statement. Then, these changes are adopted to update the set of fair states computed earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusion supported by the experimental results is presented herein.},
keywords={},
doi={},
ISSN={},
month={July},}
Copiar
TY - JOUR
TI - Incremental CTL Model Checker for Fair States
T2 - IEICE TRANSACTIONS on Information
SP - 1126
EP - 1130
AU - Victor R. L. SHEN
PY - 1999
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E82-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 1999
AB - CTL (Computation Tree Logic) model checking is a formal method for design verification that checks whether the behavior of the verified system is contained in that of the requirements specification. If this check doesn't pass, the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incremental method which successively modifies the latest verification result each time the design is modified. Our incremental algorithm allows the designer to make changes in terms of addition or subtraction of fair CTL formulas, or fairness constraints on acceptable behavior from the problem statement. Then, these changes are adopted to update the set of fair states computed earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusion supported by the experimental results is presented herein.
ER -