| 研究概要 |
ソフトウェアのモデル検査技術の応用として次の研究を行い, 発表した. 1. データベースのスキームの整合性検査，2．プログラムのループのインバリアント自動導出の精度あげるために数理解析ツールを活用する方法, JavaのequalsメソッドとhashCodeメソッドの整合性をSMTソルバーを用いて自動検証する方法．またJML, OCL相互自動変換ツールとそのオープンソフトウェアへの適用や表明カバレッジメトリクスのアイディアについて国際会議等で発表した．１についてはAlloy Analyzerを用いてフォーマルに検証する技法を用いている．2についてはMathematicaを利用することにより精度向上をめざした．3については限定モデル検査やモジュール検証の技法やZ3のビット演算機能を用いて実用的な部分クラスについて自動検証を可能とした．
またプログラムの表明導出，Alloyを用いたプログラム仕様検証，ライントレースロボットの自動検証, JML-OCL自動変換などの論文を掲載した．
|
