大規模並行実時間システムの効率的な検証方法の研究

大规模并行实时系统高效验证方法研究

• 批准号: 08750474
• 负责人: 平石 邦彦
• 金额: $ 0.38万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08750474/
• 关键词: 実時間システム; 並行システム; システム検証

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

Large-scale model and time-based monitoring of the failure rate of the monitoring method has been successful, and the following results have been successful. 1. The return action contains a negative status space agreement table to show that there is a negative impact on the status of the customer, and that the action is not affected. The use of information technology, each status of the semi-zigzag collection of information to show the performance of the system, the state of the space table to show the performance of the method of data acquisition. Please tell me that the equipment is installed and that the line is not available. Both the method and the resource information table show that there is a negative impact on the status of the space table. The data collection contains the information that contains the information, and the operating time is required to make sure that it is advantageous to collect the information. We are going to have some problems in the future. two。 The semi-sequential method of time transfer transfer is used to study each action line. It is possible to analyze the minimum price of each action line, the maximum price of each action, the maximum of the minimum, and so on. In time, it is necessary to use the semi-sequential method to determine the possible conditions for investigation. In general, it is necessary to use the possible information about the examination plan. 3. In conjunction with the status save protocol, the state space is generated. The complex action may not be affected at the same time. At the same time, it is possible to do the same. I don't know if I'm going to see you. I don't know. I don't know. I don't know. In parallel with the customer, we can collect the data and save the state space in order to generate the database research bank.

项目成果

平石邦彦: "Reduced Timed Transition Systems based on Partial Order Methods" Proc.Int.Tech.Conf.Circuits/Systems,Computer and Communications (ITC-CSCC'96). 2. 1208-1211 (1996)

Kunihiko Hiraishi：“基于偏序方法的简化定时转换系统”Proc.Int.Tech.Conf.Circuits/Systems、Computer and Communications (ITC-CSCC96)。

平石邦彦: "半順序法による並行システムの効率的な検証について" 電子情報通信学会技術研究報告. 96・204. 1-7 (1996)

Kunihiko Hiraishi：“使用偏序方法的并行系统的有效验证”IEICE技术研究报告96・204（1996）。

平石邦彦: "Reduced State Space Representation for Unbounded State Spaces" Lecture Notes in Computer Science,Springer-Verlag. 1091. 230-248 (1996)

Kunihiko Hiraishi：“无界状态空间的简化状态空间表示”计算机科学讲义，Springer-Verlag 1091. 230-248 (1996)

平石邦彦: "離散事象システムの概念と理論・応用" 計測自動制御学会システム/情報合同シンポジウム'96講演論文集. 241-246 (1996)

Kunihiko Hiraishi：“离散事件系统的概念、理论和应用”仪器与控制工程师协会联合系统/信息研讨会 96 论文集（1996 年）。