|
大規模並行実時間システムの効率的な検証方法に関して、以下の成果が得られた。
1.くり返し動作を含むような状態空間の縮約表現についての研究
ペトリネットのような状態がベクトルで表現されるようなシステムでは、ベクトル値を増加させるような動作は何回でもくり返して実行させることができる。この性質を利用して、各状態をベクトルの半線形集合の形で表現することにより、状態空間の縮約表現を得る方法について研究を行った。また、実際にアルゴリズムを実装し、評価実験を行った。この方法は、資源を状態量の1つとして表現するようなモデルの状態空間の表現においては有効であることが確認できた。しかしながら、アルゴリズムは2つの半線形集合の包含関係のチェックを含んでいるため、実行時間では必ずしも有利とはなっていない。これは今後の課題である。
2.時間付き遷移グラフへの半順序法の適用についての研究
各動作が実行可能になってから実際に実行できるまでの最小値および最大値が与えられたような実時間システムに対し、デッドロック等を保存する縮約状態空間を生成する方法について研究を行った。時間なしのモデルに対する半順序法がそのまま適用可能な条件について考察した。また、一般の場合に対しても適用可能なアルゴリズムを考案した。
3.競合状態を保存するような縮約状態空間の生成についての研究
ある状態において複数の動作が実行可能であるが同時には可能ではないときに、これらの動作は競合しているという。競合の発見はルールベース・プログラミング等の検証において重要な手がかりになる。与えられた並行プログラムにおける極大な競合集合をすべて保存するような縮約状態空間の生成について研究を行った。
|
