時間制約付きペトリネットモデルで記述された分散システムの動作仕様の自動導出

自动推导由时间约束 Petri 网模型描述的分布式系统的行为规范

基本信息

批准号：
07780260
负责人：
岡野浩三
金额：
$ 0.58万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至无数据
项目状态：
已结题

项目摘要

1.申請者らの論文"Synthesis of Protocol Entities'Specifications from Service Specifications in a Petri Net Model with Registers",Proc.of 15th IEEE International Conference on Distributed Computing Systems,pp.510-517,(1995-6).で実用的なシステムを記述するのに(時間制約を考慮にいれていないことを除いて)ほぼ充分なクラスで自動導出ができる方法を考案した.2.このクラスに対して時間制約を付加したモデルを考案した.具体的には,時間制約のモデルとして一般的なTimed Petrinetのモデルを我々のモデルに取り込むこととした.このモデルでは,時間制約として,トランジションの発火可能な状態から実際に発火するまでの最小時間と最大時間を与えている.3.このモデルとクラスのもとで,通信に一定の最大時間遅延が与えられた分散環境での実行可能性判定アルゴリズムを考案した.実行可能性の判定問題は,実数数上の線形制約式として与えられるように工夫したため,実用的な問題が十分に解ける.4.実行可能性がある際の動作仕様導出アルゴリズムを考案した.分散環境下の各実行ノードが十分に正確な内部時計を持っているという仮定のもとで,もとの仕様通りに動作する動作仕様を導出する.この動作仕様導出アルゴリズムで生成される動作仕様は一般的に時間遅延をなるべく押さえることができる.また,分散環境下での実行選択や,レジスタ値の更新競合をメッセージに時刻印を持たせる方法で解決可能であることを示した.また,本システムの導出系を作成した.5.以上の成果を平成8年3月26日に電子情報通信学会ソフトウェアサイエンス研究会にて発表する(予定).今後は,いくつかの制約条件を緩めたうえで,国際会議(ICDCS'97等)の投稿を予定している.

1。申请人的论文，“协议实体在带有寄存器的培养皿网模型中的服务规范的合成”，第15届IEEE国际分布式计算系统国际会议，第510-517页，（1995-6）。我们设计了一种允许在几乎足够的类中自动推导的方法（除了未考虑时间限制）2。我们设计了一个模型，其中添加了此类的时间限制。具体而言，定时是时间限制的常见模型。我们决定将石油公司的模型纳入我们的模型。该模型给出了从射击状态到实际射击的过渡的发射状态之间的最小和最长时间。3。在此模型和类中，我们设计了一种算法，用于确定在分布式环境中给出恒定的最大时间延迟到通信的可行性。设计可行性问题，以便将其作为对实数的线性约束，因此可以充分解决实践问题。4。我们设计了一种算法，用于在有可行性时衍生操作规格。分布式环境中的每个执行节点都具有足够准确的内部时钟。基于这样的假设，我们得出了根据原始规范运行的操作规范。此操作规范派生算法生成的操作规格通常可以抑制时间延迟。它还表明，在分布式环境中选择执行选择，并且可以通过使用消息中的时间戳来解决更新寄存器值的冲突。我们还为此系统创建了一个派生系统。5。以上的结果将于1996年3月26日在电子，信息和通信工程师的软件科学研究研究所提出。未来，我们计划在放松一些限制后在国际会议（ICDCS'97等）上发布。