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
모델 검사 기술은 신뢰성이 높은 정보 시스템을 설계하는 데 유용합니다. 그러나 잘 알려진 상태 폭발 문제는 대규모 시스템의 모델 검사에서 발생할 수 있습니다. 이러한 폭발은 모델 확인의 확장성을 심각하게 제한합니다. 이를 방지하기 위해 몇 가지 추상화 기술이 제안되었습니다. 그 중 일부는 E. Clarke가 제안한 CEGAR(CounterExample-Guided Abstraction Refinement) 루프 기술을 기반으로 합니다. et al.. 본 논문은 실시간 시스템의 모델 확인에 사용되는 Timed Automata의 구체적인 추상화 기법을 제안한다. 우리의 기술은 추상 모델을 개선하기 위한 가이드로 반례를 사용하는 CEGAR를 기반으로 합니다. 일반적으로 정제 작업은 추상 모델에 적용되지만, 우리의 방법은 원래의 시간 제한 자동 장치를 수정합니다. 다음으로, 수정된 자동장치로부터 정제된 추상 모델을 생성합니다. 이 문서에서는 알고리즘에 대한 공식적인 설명과 알고리즘의 정확성 증명에 대해 설명합니다.
모델 확인, 시간 제한 자동 장치, 모델 추상화, 시가
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.
부
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
부
@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},}
부
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 -