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