RESEARCH

研究目的
・形式的技法(formal methods)を用いたJavaプログラムの検証.
  形式的技法とは,論理学を基盤としたシステムの設計・検証技法.形式的仕様記述(formal specification)と形式的検証(formal verification)の2つからなる.
  ・形式的仕様記述
    プログラムの仕様を論理学の知識を用いて形式的に記述すること.
    形式的仕様記述言語JML(Java Modeling Language)を用いる.
・形式的検証
  プログラムが仕様を満たすことを論理的な推論により形式的に検証すること.

関連研究
名前 主な開発元 主な開発者 検証スタイル 特徴
Common JML Tools Iowa State University G.T. Leavens, Y. Cheon 自動 ランタイム検査,型検査,単体テストなど
ESC/Java(Extended Static Checker for Java) Compaq社(現Hewlett-Packard社) K. Rustan, M. Leino, G. Nelson, J. Saxe 自動 簡単な仕様を自動で検証
Calvin Compaq社(現Hewlett-Packard社) S. Qadeer, S. Freund, C. Flanagan 自動 ESC/Javaの拡張版(マルチスレッドに対応)
ChAsE(Check Assignable Expression) INRIA N. Cataño, M. Huisman 自動 ESC/Javaの拡張版(assignable clauseに対応)
ESC/Java2(Extended Static Checker for Java version 2) Eastman Kodak社, University College Dublin D.R. Cok, J. Kiniry 自動 ESC/Javaの強化版
Krakatoa INRIA C. Marché, C. Paulin, X. Urbain 対話型 定理証明器Coqを用いた対話型検証
LOOP University of Nijmegen J.v.d. Berg, B. Jacobs, E. Poll 対話型 定理証明器PVSを用いた対話型検証
Jive University of Kaiserslautern A. Poetzsch-Heffter, P. Müller 対話型 定理証明器Isabelle/HOLを用いた対話型検証
KeY University of Karlsruhe, University of Koblenz, Chalmers University of Technology W. Ahrendt 対話型 定理証明器KeY Proverを用いた対話型検証
JACK(Java Applet Correctness Kit) Gemplus社(現在はINRIAが開発) L. Burdy 自動/対話型 自動定理証明(対話型検証も可能)
SpEx(Specifications Exploration) Kansas State University M. Robby, M.B. Dwyer, J. Hatcliff 自動 モデル検査ツールBogorを用いた検証
Daikon MIT M.D. Ernst - ソースコードからJML仕様を自動生成
Eiffel Interactive Software Engineering社(現Eiffel Software社) B. Meyer - DbCを実装するオブジェクト指向型プログラミング言語
Bali Technical University of Munich G. Klein, T. Nipkow, D.v. Oheimb, N. Schirmer, L.P. Nieto - 定理証明器Isabelle/HOL上でのJava Card言語の意味論の形式化

勉強中
・formal methods
Gemplus' electronic purseの検証
  ・Decimalクラスの検証
    ・mulメソッド(検証中 proof obligationがCoqでエラー loop不変条件が証明できない プログラムの除算と定理証明系内の除算の意味の違い?)
    ・addメソッド(検証済み ※実装を変更)
    ・opposeメソッド(検証済み)
・その他の検証例
  selection sortの検証(検証中 メモリ関係のsubgoalが2つ残る)
  insertion sortの検証(検証中 loop不変条件が証明できない)
・ツールの信頼度のレベルと要求される安全性のレベルの対応付け(KrakatoaとESC/Javaの中間?)
・定理証明系のフィードバック
・Bali(中断)
・モデル検査技法(済)
・push up postconditionの実装(進行中 字句解析部分を実装中)
・JACK(進行中  proof obligationの生成は可能だが,証明タスクの実行方法が不明)
・Hoare論理の意味論

その他
中間発表スライド(060908)
中間発表配布資料(060908)
研究室紹介スライド(061004)
中間発表スライド(061226)