情報処理学会 第81回全国大会講演要旨

形式手法の1つとして、仕様記述からコード生成までを支援するB Methodがあり、これは数学的な仕様とその詳細である実装、及びそれらの中間的記述であるリファインメントからなる。これらを分解し部品として再利用することによって、高信頼ソフトウェアを低コストで生成する手法を提案しているが、従来手法ではリファインメントが考慮されていなかった。
そこで本研究では、リファインメントを考慮した部品生成手法と結合手法を提案する。しかしリファインメントの段数や変数の詳細化順序の不一致などにより問題が生じるため、変数間の関係を示すリンク不変条件を利用することでこれらの問題を解消する。