モデル検査技術を利用したプログラム解析器の生成ツール

機関リポジトリ 情報処理学会 Web Site 被引用文献5件 参考文献12件

書誌事項

タイトル別名
  • モデル ケンサ ギジュツ オ リヨウ シタ プログラム カイセキキ ノ セイセイ ツール
  • Generation of Program Analyzer Based on Model Checking

この論文をさがす

抄録

本論文では,時相論理式によって仕様が記述されたプログラム解析をモデル検査技術の利用によって行うツールについて述べる.本ツールは,対象プログラム言語はJimple,プログラム解析の仕様記述言語は時相論理CTL-FVである.JimpleはJavaと相互変換可能な3番地コードからなる中間言語であり,Javaに比ベプログラム解析や最適化が適用しやすい.また,CTL-FVはCTL(Computation Tree Logic)を拡張した時相論理であり,プログラム中の情報を述語に引用することを許したところに大きな特徴がある.CTL-FVによって多くのプログラム解析が記述できるため,本ツールを使用するとJimpleプログラムに対し様々な解析を自動的に行うことができるようになる.今回,モデル検査を既存のモデル検査ツールSMVをそのまま利用することによって実装が非常に簡単になり,Java言語で約500行(コメント除く)のプログラムでこれが実現できた.また,標準ライブラリのいくつかのクラスに対して無用命令の検出を本ツールにより実行したところ,比較的大きなサイズのクラスに対しても数分で解析することができた.ここでは,主に本ツールの設計と実装について説明する. : In this paper, we describe a tool that automatically performs program analysis using model-checking techniques. The tool has two characteristics; the target program is Jimple, and the specification of program analysis is described in temporal logic CTL-FV. Jimple is mutually convertible with Java; it is a 3-address intermediate language and is easier to perform program analyses and optimizations than Java. CTL-FV is an extension of CTL (Computation Tree Logic) to allow quoting information in a program to formulas. CTL-FV can describe many program analyses, thus our tool can carry out various analyses automatically. By the use of the well-developed model- checker SMV, we implemented this tool with only 500 lines of code in Java. As an example, dead code detection is performed to some classes in the standard library, and relatively large classes can be analyzed in a few minutes. We explain the design and the implementation of the tool.

identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/4566

収録刊行物

被引用文献 (5)*注記

もっと見る

参考文献 (12)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ