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
Les techniques de vérification de modèle sont utiles pour la conception de systèmes d'information hautement fiables. Le problème bien connu de l’explosion d’état pourrait cependant se produire lors de la vérification de modèles de grands systèmes. Une telle explosion limite considérablement l’évolutivité de la vérification des modèles. Afin de l'éviter, plusieurs techniques d'abstraction ont été proposées. Certains d'entre eux sont basés sur la technique de boucle CounterExample-Guided Abstraction Refinement (CEGAR) proposée par E. Clarke. et al.. Cet article propose une technique d'abstraction concrète pour les automates temporisés utilisée dans la vérification de modèles de systèmes temps réel. Notre technique est basée sur CEGAR, dans laquelle nous utilisons un contre-exemple comme guide pour affiner le modèle abstrait. Bien que, en général, l’opération de raffinement soit appliquée à des modèles abstraits, notre méthode modifie l’automate temporisé original. Ensuite, nous générons des modèles abstraits raffinés à partir de l'automate modifié. Cet article décrit les descriptions formelles de l'algorithme et la preuve de l'exactitude de l'algorithme.
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.
Copier
Takeshi NAGAOKA, Kozo OKANO, Shinji KUSUMOTO, "An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop" in IEICE TRANSACTIONS on Information,
vol. E93-D, no. 5, pp. 994-1005, May 2010, doi: 10.1587/transinf.E93.D.994.
Abstract: Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E93.D.994/_p
Copier
@ARTICLE{e93-d_5_994,
author={Takeshi NAGAOKA, Kozo OKANO, Shinji KUSUMOTO, },
journal={IEICE TRANSACTIONS on Information},
title={An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop},
year={2010},
volume={E93-D},
number={5},
pages={994-1005},
abstract={Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.},
keywords={},
doi={10.1587/transinf.E93.D.994},
ISSN={1745-1361},
month={May},}
Copier
TY - JOUR
TI - An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
T2 - IEICE TRANSACTIONS on Information
SP - 994
EP - 1005
AU - Takeshi NAGAOKA
AU - Kozo OKANO
AU - Shinji KUSUMOTO
PY - 2010
DO - 10.1587/transinf.E93.D.994
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E93-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2010
AB - Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
ER -