学術雑誌論文

学術雑誌論文

text

IEICE TRANSACTIONS on Information and Systems. 2010, E93-D(5), p. 994-1005

An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop

英語

text

2010-05-01

https://doi.org/10.1587/transinf.E93.D.994

http://search.ieice.org/

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.

Copyright © 2010 The Institute of Electronics, Information and Communication Engineers

27452

An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop

電子情報通信学会

英語

2010-05-01

IEICE TRANSACTIONS on Information and Systems

E93-D

5

994

1005

https://doi.org/10.1587/transinf.E93.D.994

https://hdl.handle.net/11094/27452

http://search.ieice.org/