|
家庭用電気製品の制御のためのマイクロプロセッサ用に開発されたアセンブリー言語のプログラムを題材として取り上げ、プログラム理解の枠組みについて検討した。これまでの成果によって、基本的な枠組みはほぼ明らかになっていたが、実機器向けのある程度複雑な制御をおこなうプログラムを対象とした有効性を確認する必要があった。まず、予備的調査により、割り込みなどのOSの機能をある程度考慮したプログラム理解系が必要であることがわかった。そこで、割り込みに対する処理を検討し、従来のプログラム理解の枠組みの中に組み入れるための方法を検討した。
また、プログラム理解の結果をプログラム開発の中で有効に役立てるための仕組みについて検討した。プログラム開発の流れの中で、これまで有効な支援ツールが提供されていなかった部分に、機械の要求仕様に対してプログラムが正しく構成されているかを検証するフェーズがある。このフェーズで問題になる要求仕様は、機械の動作に関する断片的な制約条件の羅列であり、プログラムの構成とは全く無関係と言っても過言ではない。本研究では、そのような制約が機械の状態遷移に関する4タイプの表現と、状態遷移に関わる定量的制約とに集約して再構成可能であることを示し、そのように再構成された制約表現をもとに、プログラムの動作を確認、検証するための基本的なアルゴリズムを検討した。
以上の2つの成果の基づいて、実験的なシステムを構築している。現在までに主要な部分は実現できているが、細部の調整までは至っていない。さらに、実験システムを用いたプログラムの検証実験と評価については、今後の課題である。
|
