現実的な形式的オブジェクト指向分析と計算機支援環境

点击翻译按钮获取中文摘要

高い信頼性を持つシステムを実現するためには、形式的手法の導入が必要であるが、冗長性などの問題が障壁となり、実際のシステム開発に適用されていない。そこで、本研究では、この問題点を(1)領域ライブラリの作成による再利用性の向上、(2)オブジェクト指向分析モデルの構文面の性質の自動検証、により解決する。(1)、(2)の成果は、それぞれ、以下のとおりである。(1)領域ライブラリの作成による再利用性の向上。本研究の成果として、領域ライブラリのためのモデル、公理系、定理証明システムHOLによる支援法について提案した。提案したモデルでは、対象領域に出現する概念をクラス図を用いてモデル化する。構築したモデルは、提案した公理系によりオブジェクト指向分析モデルの様々な性質の検証に用いることができる。また、公理系を、定理証明システムHOLにより取り扱い可能な形式に翻訳する手法を提案した。これにより、構築した領域ライブラリを用いて、定理証明システムHOL上でオブジェクト指向分析モデルの様々な性質を検証することが可能になった。領域ライブラリは、同一の性質を持つ複数のシステムに共通な概念をライブラリ化したものである。提案したこれらの成果を用いて検証のための領域ライブラリを作成することにより、コストが高く障壁となっていた検証に伴う証明の再利用性が向上し、形式的検証が現実的なものとなることが期待される。(2)オブジェクト指向分析モデルの構文面の性質の自動検証。本研究では、構築したモデルの構文面の性質を自動的に検証するツールを作成した。このツールでは、Rational Rose等の市販のツールにより構築したモデルをUMLXMI形式で読み込み、OCLにより記述した構文面の性質を自動検証する。このような構文面の性質は、(1)で提案した手法を適用するまでもなく、自動的に検証可能である。実際、他論文で提案されている構文面の性質を、提案したツールで自動的に検証可能であることを確認した。本研究により提案した(1)、(2)の手法を適切にシステム開発に適用することにより、検証コストを低く抑えることが可能になる。これにより、実際のシステム開発に形式的手法を導入することが可能になり、製品の信頼性の飛躍的な向上が期待される。