Common System Descriptions を用いたシステム記述
小田 伸司 (9551019)
この論文ではさまざまな様式のソフトウェアを共通の記述から一貫した体系で開発する
システム開発の新手法を提案している。この手法では、システムの仕様は Common
System Descriptions (CSD) という形式で記述される。CSD は核となる仕様と
それぞれの実装向けの仕様とに分かれている。まず核となる仕様が記述され、それを
基にそれぞれの実装向けの仕様が記述される。CSD は形式的仕様記述言語で記述され、
形式的手法に基づく各仕様間の関係においてそれぞれの実装の一貫性が保証されて
いる。
この論文ではまた CSD を用いたソフトウェア開発の具体例について示している。
簡単な電卓のシステムを形式的仕様記述言語 RAISE specification language (RSL) を
用いて記述し、それをラピッドプロタイピングとしての関数型言語 ML への実装および
ハードウェアへの実装を視野に入れた形式での手続型言語 C による記述を行った。
また、形式的証明および実装されたソフトウェアの実行による開発の一貫性の検証
および確認を行なった。