リアルタイムシステムのための階層的時間検証方式に関する研究

实时系统分层时间验证方法研究

• 批准号: 05780233
• 负责人: 米田 友洋
• 金额: $ 0.7万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-05780233/
• 关键词: 検証; リアルタイムシステム; タイムペトリネット; 階層的検証; 状態爆発; 時間トレース理論

本研究では,実時間制約を持つシステムの検証を階層的に行い,非常に高効率な時間検証方式を開発することを目的とする.本研究の成果は以下の3点である.(1)仕様および検証対象システムをタイムペトリネットを用いてモデル化することとし,スタンフォード大のD.Dillらによる,ペトリネットに基づく検証方式をベースに検証アルゴリズムを開発した.Dillらの方式は,非同期式回路の(時間を含まない)性質の検証が目的であり,実時間は扱えない.そこで,Dillらのアルゴリズムの根底をなすトレース理論を拡張し,時間トレース理論を提案した.これにより,実時間制約を持つシステムのsafety性のほか,Dillらの方式では容易には扱えなかった(ある種の)liveness性も容易に扱えるようになった.(2)時間トレース理論に基づき,仕様および検証対象システム(いくつかのモジュールから成る)を表すいくつかのタイムペトリネットの状態空間を探索し,各可到達状態がsafetyあるいはlivenessに反していないかどうかを調べるアルゴリズムを開発した.また,実際にインプリメントした.(3)いくつかの例を用いて検証を行った結果,確かに階層的検証により大幅に検証時間を削滅できることがわかったが,一状態あたりの処理にやや時間がかかり過ぎるという問題が見つかった.検討の結課,状態を表す連立一次不等式の標準形を求めるのにかなりの時間がかかっていることがわかった.そこで,タイムペトリネットの状態を表す連立一次不等式の特殊性に着目し,従来用いていたO(n^3)のアルゴリズムを改良し,O(n^2)のアルゴリズムを開発した.以上より,本研究の目的はほぼ達成できたが,さらに効率を向上するため,不要な順序関係を生成しないように状態探索を行うというpartial orderの考え方を導入し,アルゴリズムを改良することが今後の課題である.

This study aims to develop a very efficient and time-constrained approach to the identification of multiple layers of evidence. The results of this study are as follows: (1)The method of identification of the object type is to detect the loss of the object type, and the method of identification of the property of the asynchronous loop is to detect the loss of the object type. The basic theory of Dill's theory is to expand the theory of time. The time limit for this is the safety of the system, and the way to do it is easy to do it is easy to do it. (2)Time theory is based on the theory of time, and the state space of each reachable state is explored in the table of time and the state space of each reachable state is explored in the table of time and the state space of time. In the meantime, I'm going to have to ask you a few questions. (3)For example, if you use the test to verify the results of the test, you can verify the level of the test. If you use the test to verify the time, you can reduce the time. If you use the test to process the test, you can see the problem. The standard form of a linear inequality is obtained by means of a state table. In this paper, the state of O(n^3) and O(n^2) is introduced. The purpose of this study is to achieve the above goals, and to improve the efficiency of the system.