| 研究概要 |
平成19年度は,モジュラーな項書換システムの研究を引き続き行い,より簡明な理論の構築と実装に向けての検討を行った.またモジュラーな検証システムと他の検証システムとの協調的な検証技術の構築のための基礎研究として,項書換システムによる等式推論を基礎とする証明スコアによる手法以外の代数仕様の検証技術に関する研究を行った.
モジュラーな項書換システムの理論は,マカオで開催された国際会議The 4th International Colloquium on Theoretical Aspects of Computingで発表し,計算機科学のレクチャーノート(LNCSシリーズ)に掲載された.書換理論,仕様記述,検証技術を含む計算機科学の理論的な側面からの最新の研究発表が多くなされ,本研究課題の今後の方向性を考える上で重要な機会となった.
他の検証ツールとの協調に関する研究として,不動点の概念を用いた振舞仕様の不変性自動検証ツールCremeの研究開発を行った.今後はCremeで扱いやすい問題の分析を行い,どのようにモジュラーな検証エンジンに取り込むかを検討する.振舞仕様から書換仕様への変換手法の提案も行い,振舞仕様へのモデル検査技術の適用を可能とした.また検証エンジンの振舞の分析のための研究として,代数仕様のための停止性判定手法の提案を行った.代数仕様記述者が扱いやすい停止性判定手法の提案は,モジュラーな検証エンジンに適切な代数仕様の作成方法へとつながる重要な基礎研究である.
|
