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

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14019044
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702)
• Co-Investigator(Kenkyū-buntansha): 片山 卓也 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)
• Keywords: オブジェクト指向分析 / 形式的手法 / 検証 / 計算機支援環境

Research Abstract

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

Research Products

• [Publications] 矢竹健朗, 青木利晃, 片山卓也: "定理証明システムHOLにおけるオブジェクト指向理論の構築"情報処理学会ソフトウェア工学研究会研究報告書 2002-SE-138. (2002)
• [Publications] 青木利晃, 片山卓也: "オブジェクト指向分析モデルの検証支援環境"日本ソフトウェア科学会全国大会. (CD-ROM). (2002)
• [Publications] Takaaki Tateishi, Toshiaki Aoki, Takuya Katayama: "Successive Behavior Approximation Method for Verifying Distributed Objects"Proc. Third International Conference on Parallel and Distributed Computing, Application and Technologies. 439-446 (2002)
• [Publications] Mitsutaka Okazaki, Toshiaki Aoki, Takuya Katayama: "Extracting Threads from Concurrent Objects for the Design of Embedded Systems"Proc. Asia-Pacific Software Engineering Conference APSEC2002. 107-116 (2002)
• [Publications] 立石孝彰, 青木利晃, 片山卓也: "振舞い近似手法を用いたステートチャートに対する不変性の検証"情報処理学会論文誌「オブジェクト指向技術特集」. 44巻6号. (2003)
• [Publications] Mitsutaka Okazaki, Toshiaki Aoki, Takuya Katayama: "Formalizing Sequence Diagrams and State Machines Using Concurrent Regular Expression"Proc. Second International Workshop on Scenarios and State Machines : Models, Algorithms and Tools, ICSE2003 Workshop. (2003)