Practical Program Validation for State-Based Reactive Concurrent Systems : Harmonization of Simulation and Verification

スポンサーリンク

概要

• 論文の詳細を見る

• This paper proposes a practical method of program validation for state-based reactive concurrent systems. The proposed method is of particular relevance to plant control systems. Plant control systems can be represented by extended state transition systems (e.g., communicating asynchronous transition systems). Our validation method is based on state space analysis. Since naive state space analysis causes the state explosion problem, techniques to ease state explosion are necessary. One of the most promising techniques is the partial order method [10]. However, these techniques usually require some structural assumptions and they are not always effective for actual control systems. Therefore, we claim integration and harmonization of verification (i.e., state space analysis based on the partial order method) and simulation (i.e., conventional validation technique). In the proposed method, verification is modeled as exhaustive simulation over the state space, and two types of simulation management techniques are introduced. One is logical selection (pruning) based on the partial order method. The other is heuristic selection based on priority (a priori precedence) specified by the user. In order to harmonize verification (logical selection) and conventional simulation (heuristic selection), we propose a new logical selection mechanism (the default priority method). The default priority method which prunes redundant state generation based on default priority is in harmony with heuristic selection based on the user's priority. We have implemented a practical validation tool, Simulation And Verification Environment for Reactive Concurrent Systems (SAVE/RCS), and applied it to chemical plant control systems.

• 社団法人電子情報通信学会の論文
• 1995-11-25

著者

• Uchihira Naoshi

  System Engineering Laboratory Of Corporate Research And Development Center Toshiba Corporation

• Uchihira Naoshi

  Systems & Software Engineering Laboratory Research & Development Center Toshiba Corporation

• Kawata Hideji

  Systems & Software Engineering Laboratory, Research & Development Center, Toshiba Corporation

• Kawata H

  Nec Saitama Ltd. Saitama‐ken Jpn

関連論文

• Software Prototyping with Reusable Components
• Practical Program Validation for State-Based Reactive Concurrent Systems : Harmonization of Simulation and Verification
• Special Section on Concurrent System Technology
• A High-Level Petri Net for Accurate Modeling of Reactive and Concurrent Systems (Special Section on Description Models for Concurrent Systems and Their Applications)

スポンサーリンク