Design Verification of Sequential Control Circuits Based on Theorem-Proving Method
スポンサーリンク
概要
- 論文の詳細を見る
VSEQ (Verifier for SEQential controller) is a design verification system for sequential control circuits in an electric power substation. Instead of using the prevailing simulation techniques, it verifies the design by using a theorem-proving method, which does not need any test data generation and guarantees reliable verification. Thus VSEQ realizes a theorem-proving method dedicated to the design verification of sequential control circuits. This paper shows that use of domain characteristics in the formulation of the verification problem and also in control of the proof process leads to a theorem-proving method that is efficient enough for practical design verification.
- 一般社団法人情報処理学会の論文
- 1991-07-31
著者
-
MATSUDA Satoshi
Department of Ophthalmology, University of Tokushima School of Medicine
-
Yamada N
Energy Research Laboratory Hitachi Ltd.
-
Ueda Yoshikatsu
Systems Engineering Division Hitachi Ltd.
-
Matsuda S
Kyoto Univ. Kyoto Jpn
-
KOBAYASHI YASUHIRO
Energy Research Laboratory, Hitachi Ltd.
-
Yoshizawa Junichi
Computer & Communication Research Center, The Tokyo Electric Power Co.
-
Yamada Naoyuki
Energy Research Laboratory Hitachi Ltd.
-
MATSUDA SATOSHI
Computer & Communication Research Center, The Tokyo Electric Power Co.
-
MUTO SHOUICHI
Computer & Communication Research Center, The Tokyo Electric Power Co.
-
Yoshizawa Junichi
Computer & Communication Research Center The Tokyo Electric Power Co.
-
Muto Shouichi
Computer & Communication Research Center The Tokyo Electric Power Co.
-
Kobayashi Yasuhiro
Energy Research Laboratory Hitachi Ltd.
関連論文
- Ocular Activity of Topically Administered Anandamide in the Rabbit
- ROLE OF ICAM-1 AND LFA-1 IN ENDOTOXIN-INDUCED UVEITIS IN MICE
- c-Jun N-terminal kinase activation during warm hepatic ischemia/reperfusion injuries in a rat model
- FRS-024 Interaction of Scaffolding/Docking Protein Gab1 with Tyrosine Phosphatase SHP2 Is Involved in gp130-dependent Activation of ERK5 and Elongation of Cardiomyocytes(Cardiac Hypertrophy (M) : FRS3)(Featured Research Session (English))
- Induction of Connective Tissue Growth Factor in Retinal Pigment Epithelium Cells by Oxidative Stress
- The Migdal-Kadanoff Transformations on the Dual Lattice : Particles and Fields
- A Knowledge Compilation Method Through Conversion of Symbolic Rules and Facts into Functions
- Design Verification Based on Theorem-Proving Technique for Sequential Control Circuits with Timing Coordination
- Two-Way Quark-Cascade and Band Structure in P + Be^9→(h^+h^-X, h^+h^+X, h^-h^-X)
- Design Verification of Sequential Control Circuits Based on Theorem-Proving Method
- A Plant Diagnosis Method Based on the Knowledge of System Description
- A Knowledge Acquisition Method Based on a Multi-Attribute Utility Model
- A Theorem Proving System for Logic Design Verification
- Meson-Baryon and Baryon-Antibaryon Ratios in Two Way Quark-Cascade Model
- Oscillator Representation of Virasoro Algebra and Kac Determinant
- Is a Charmed Axial-Vector Meson Already Found?
- The Dual Symmetry and the Migdal-Kadanoff Recursion Equations
- Two Way Quark-Cascade and Particle Ratios in γ+P → h^±+Anything
- Logic Verification System for Power Plant Sequence Diagrams.
- Sensitivity study of fuel cost in extended burnup BWR core.
- Approach to knowledge based man-machine communication for BWR start-up guidance.