高階木変換器の自動検証のための反例発見と抽象化改良  [in Japanese] Counterexample Finding and Abstraction Refinment for Automated Verification of Higher-Order Tree Transducers  [in Japanese]

Access this Article

Author(s)

Abstract

近年,Kobayashiらは高階木変換器HMTTの検証手法を提案した.HMTTは高階関数型木構造処理プログラムの一種であり,その検証の目的は,HMTTが与えられた入出力木の仕様を満たすか否かを判定することである.彼らの手法では,木構造データを入出力仕様を表すオートマトンを用いて抽象化することにより,HMTT検証問題を高階モデル検査問題に帰着させる.しかしながら,彼らの手法では,検証に失敗した場合に実際に仕様に対する反例があるのか否かを判断することができなかった.そこで,本論文では,帰着後の高階モデル検査問題に対する反例を用いて対応するHMTT検証問題の反例を構成する方法を示す.また,対応する反例が存在しない場合に抽象化に用いるオートマトンの状態を分割し,検証の精度を改良する方法を提案する.さらに提案手法に基づいてHMTT検証器を改良し,その有効性を示す実験結果を報告する.

Kobayashi et al. recently proposed a method for verification of higher-order tree transducers called HMTTs. An HMTT can be considered as a higher-order, functional tree-processing program. The goal of the HMTT verification is to check whether a given HMTT satisfies a given input/output specifications. Kobayashi et al.'s algorithm abstracts tree data using automata that represents input/output specifications and reduces an HMTT verification problem to a higher-order model checking problem. Their method cannot, however, determine whether a given HMTT verification problem actually has a counterexample when a corresponding higher-order model-checking problem has a counterexample. We propose a method of generating a counterexample of an HMTT verification problem from a counterexample of a corresponding higher-order model-checking problem. We also propose a method of refining an abstraction by splitting the states of automata when counterexamples do not exist. We have implemented the method and report the effectiveness of the method.

Journal

  • Computer Software

    Computer Software 32(1), 1_161-1_178, 2015

    Japan Society for Software Science and Technology

Codes

Page Top