|
本年度は、実現不能な仕様の欠陥情報を用いて部分プログラムを合成するための基礎として、欠陥情報の検出方式の形式化を行なった。
●仕様の充足不能性を効率的に検証する手続きとして、前段階での検証時に生成したタブローを用いて現段階での検証を行なう発展型のタブロー法の構成を行なった。充足不能性は実現可能な仕様が満たすべき性質の中でも基本的なものである。
●有限フレームを意味とする様相論理に特化した分解証明法の構成を行なった。ここでの様相論理はシステムが止ることをフレームの制約として持つものである。この論理と通常の時間論理の証明システムにおいては、無限状態列をどのように標準化して検証を行なうかという共通の問題がある。本研究においては、無限列に対する無矛盾性の判定を、(標準化された)有限列の繰り返しに対する無矛盾性判定で行なえることの正当性が示され、その標準化モデルに基づく証明法が示された。
●メールの中継のためのリアクティブシステムの実装を実際に行なった。これは、ファイアーウォールを導入したネットワークにおいて、出先でのユーザに対して安全かつ利便なメール送信のためのシステムを提供するものである。
ここで取り扱われる中継のためのプロトコルは単純なので、本研究での仕様と検証における実例として使いたいと考えている。
|
