機能に基づく仕様のコンポーネント化を可能とする形式仕様言語の開発

1999 Fiscal Year Annual Research Report

• Project/Area Number: 10558043
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Kenkyū-buntansha): 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991) ; 渡部 卓雄 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (20222408)
• Keywords: コンポーネント / オブジェクト指向 / CafeOBJ / 形式仕様 / 振舞い仕様 / 検証 / 方法論 / 閲覧システム

Research Abstract

本年度は,以下のことを行った。
・コンポーネントの合成による仕様記述および検証:形式仕様記述言語CafeOBJのための,仕様のコンポーネント化のための基礎技術を開発した。この基礎技術にもとづいて仕様を記述することで,コンポーネントの仕様記述のみならず,検証をも再利用することができる。また,この仕様作成および検証方法は,オブジェクト指向によるソフトウェア開発との相性がよい。
・コンポーネントの合成により作成した仕様の閲覧システム:上記の仕様作成方法に則り,ODP Trading Functionの仕様を記述し,その仕様の閲覧システムを作成した。
・コンポーネントの合成により作成した仕様の自動検証:コンポーネントの合成方法に制限を設ける(オブジェクト合成と呼ぶ)ことで,合成により作成した仕様の自動検証を可能にした。ここで意味する検証とは,合成により作成した仕様が,与えた基本仕様の詳細化になっていることの確認である。
・鉄道信号システムの仕様記述と検証:コンポーネントの合成による仕様記述に基づいて,分散システムの一例である鉄道信号システムの仕様を記述し,鉄道信号システムの安全性(列車追突のないこと)を検証した。コンポーネントの合成により仕様を作成することで,仕様の再利用性を促進できたことを確認できた。

Research Products

• [Publications] R.Diaconescu,K.Futatsugi,S.Iida: "Component-based algebraic specification and verification in CafeOBJ"Lecture Notes in Computer Science. 1709. 1644-1663 (1999)
• [Publications] C.Matsumiya,S.Iida,K.Futatsugi: "A component-based algebraic specification of ODP trading function and the interactive browsing environment"Proc.of OBJ/CafeOBJ/Maude at Fprmal Methods'99. 227-241 (1999)
• [Publications] M.Matsumoto,K.Futatsugi: "Object composition and refinement by using non-observable projection operators: a case study of the automated teller machine system"Proc.of OBJ/CafeOBJ/Maude at Fprmal Methods'99. 133-157 (1999)
• [Publications] M.Matsumoto,K.Futatsugi: "Simply Observable Behavioral Specification"Proc.of Asia-Pasific Software Engineering Conference. 460-467 (1999)
• [Publications] 清野貴博,緒方和博,二木厚吉: "代数仕様言語CafeOBJによる鉄道信号システムの記述と検証"ソフトウェア工学の基礎VI(日本ソフトウェア科学会FOSE'99). 180-187 (1999)