研究内容

形式的仕様記述を利用したソフトウェア開発

　形式的仕様記述を利用したソフトウェア開発に関する研究を行ってきている。特に形式的仕様記述法のひとつである代数的仕様記述法を利用し、信頼性の高いソフトウェアを効率的に開発する方法について研究を行ってきた。代数的仕様ではデータを代数として捉え、データ間の関係を等式で記述する。厳密な仕様が記述できる反面、習得が難しく、その記述や読解に手間がかかる。そこで、代数的仕様の記述性、読解性を高める必要がある。これまでに、代数的仕様の記述性を高めるために、エラー記述の不足した仕様に対してエラー記述を自動付加する方法について研究してきた。また、代数的仕様とそれに基づいて実現されたプログラムを対象とし、仕様の変更をプログラムに反映し、仕様とプログラムの整合性を保つ方法について研究してきた。
現在は、代数的仕様を利用したソフトウェアの移植支援に関する研究を行っている。計算機システムは多様なプラットフォームで使用されるようになっており、ひとつのソフトウェアを様々なプラットフォームへ移植する作業が多く行われている。ある利用環境で運用されているソフトウェアを異なる環境で使用するためには、環境に応じた改変が求められる。このような適合化のためにソフトウェア全体に大幅な変更を加えることも多く、開発コストの増大を招いている。また、システムの開発サイクルは従来に比べ短くなってきており、開発速度の向上が求められている。計算機システムの開発期間を短縮し、開発コストを減らすためにはソフトウェア移植の負担軽減が必要となる。そこで、ソフトウェア移植コストの減少とシステムの開発速度の向上を図るため、形式性に優れた代数的仕様を利用したソフトウェア移植支援法を確立し、移植支援環境の実現をめざして研究を行っている。
ソフトウェアの仕様はプラットフォームが変更になったとき、プラットフォームに依存する部分を変更する必要がある。本手法では、ソフトウェアの仕様を記述したソフトウェア仕様に加え、プラットフォームの仕様を代数的に記述したプラットフォーム仕様を用いて移植支援を行う。プラットフォーム仕様にはAPIの仕様やハードウェアの違いによるパラメータの制限などが記述される。ソフトウェア仕様とプラットフォーム仕様の両方に代数的仕様記述法を用いることで、整合性を保持した移植が可能となる。プラットフォーム仕様はプラットフォームごとに一つ用意すればよい。
本手法の移植支援環境を用いて、あるプラットフォーム上で開発されたソフトウェアの仕様とそのプログラムを別のプラットフォームに移植する手順は以下のとおりである。
１．プラットフォーム仕様の差分の抽出
２．プラットフォーム仕様差分に基づいたソフトウェア仕様の自動変更
３．ソフトウェア仕様の差分とプログラムからプログラムテンプレートの生成
ソフトウェアを異なるプラットフォームに移植するときは、まず移植元と移植先のプラットフォーム仕様の差分を抽出する。これにより、たとえばプログラムが利用しているAPIの違いが抽出できる。そして、ソフトウェア仕様とプラットフォーム仕様の整合性を調べることで、移植先のプラットフォームに適合するようにソフトウェア仕様を変更する。たとえば、プラットフォームによって異なるAPIを利用している部分が変更されることになる。ソフトウェア仕様の変更前後の差分と移植元のプログラムからプログラムテンプレートの生成する。
プログラムを自動変更することが望ましいが一般的には困難であるため、プログラムテンプレートの生成する。
プラットフォームに依存しないように記述したソフトウェア仕様も新しいプラットフォームに適合しようしたときに、プラットフォームの持つ制限と矛盾を起こす可能性がある。このような矛盾を仕様のレベルで検出する方法を確立する必要がある。