Implementation of Stepwise Satisfiability Checker for Reactive System Specifications using Distributed Objects Technology
スポンサーリンク
概要
- 論文の詳細を見る
The realizability is a well known property for reactive system specification, and it shows that there exists a system which reacts properly against any environment following the specification. In system development process, we can reduce reversions if realizability for specification is verified before implementation of system. However, the verification cost is too high to verify the realizability of a real scale system specification. On the other hand, stepwise satisfiability which is a necessary condition for the realizability has been proposed. Its verification cost is less than that of realizability, and verification of the property is useful to find the incompleteness of specification. Even if the verification of stepwise satisfiability, the required cost is too high. In order to overcome this problem, this paper proposes methods of implementing the stepwise satisfiability checker using a distributed object technology on the parallel distributed environment. Then, we implement the stepwise satisfiability checker in Java based on our methods, and confirm the effectiveness of our methods by experiments. In this paper, we present our ideas and methods of the implementations for three parts of our checker. The first is how our checker compose a tableau graph on the parallel distributed environment. The second is the implementation method to determinize the distributed graph. The third is the dead end checking method for the deterministic distributed graph.
論文 | ランダム
- 炭化水素からL-グルタミン酸醗酵のスケールアップに関する研究
- PVAフィルターの空気中雑菌の捕集効率について
- 高粘性液の酸素移動
- 325 連続攪拌槽内における油滴分裂速度
- 324 醗酵槽内の流動特性 : 乱流強度の測定