In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. E78-A, No. 11, pages 1487-1497. 1995.
Abstract: 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). The proposed validation method is based on state space analysis. Since naive state space analysis causes the state space explosion problem, techniques to ease state space explosion are necessary. One of the most promising techniques is the partial order method. However, these techniques usually require some structural assumptions and they are not always effective for actual control systems. Therefore, integration and harmonization of verification (i.e., state space analysis based on the partial verification method) and simulation (i.e., conventional validation technique) is proposed. In this method, verification is modeled as exhaustive simulation over the state space, and two types of simulation management technique 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), a new logical selection mechanism (the default priority method) is proposed. 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. A practical validation tool, Simulation And Verification Environment for Reactive Concurrent Systems (SAVE/RCS) has been implemented and applied to chemical plant control system.
Keywords: SAVE/RCS, exhaustive simulation, formal verification, partial order method, plant control systems, reactive concurrent systems, state transition systems.