Design Verification Based on Theorem-Proving Technique for Sequential Control Circuits with Timing Coordination

スポンサーリンク

概要

• 論文の詳細を見る

• A design verification method for sequential control circuits with timing coordination has been developed. Unlike prevailing numeric simulations, this method is based on a theorem-proving technique. Sequential control circuits realize their target functions by coordinating the asynchronously inputted signals. In drder to verify timing coordination efficiently, the control strategy which combines hyperresolution and a connection graph method with attached procedures for handling time variables symbolically has been developed. This method facilitates not only the verification of timing coordination but also the extraction of intended behaviours from proposed designs. The developed method was applied to verificauon of an auto-recloslng crrcurt In an electnc power substation which contains about 40 components. The verification for each specification was executed correctly in about I minute on a mainframe computer. The developed verification method was udged to be useful and efficient for practical use.

• 一般社団法人情報処理学会の論文
• 1994-12-15

著者

• MATSUDA Satoshi

  Department of Ophthalmology, University of Tokushima School of Medicine

• Ito J

  Laboratory Of Biochemistry Sagami Women's University

• Yamada N

  Energy Research Laboratory Hitachi Ltd.

• Ueda Yoshikatsu

  Systems Engineering Division Hitachi Ltd.

• Nakamura Tomoharu

  Kokubu Works Hitachi Ltd.

• Matsuda S

  Kyoto Univ. Kyoto Jpn

• Yamada Naoyuki

  Energy Research Laboratory, Hitachi, Ltd.

• Ito Junko

  Systems Engineering Division, Hitachi, Ltd.

• Yoshizawa Junichi

  Computer & Communication Research Center, The Tokyo Electric Power Co.

• Mastuda Satoshi

  Computer & Communication Research Center, The Tokyo Electric Power Co.

• Yamada Naoyuki

  Energy Research Laboratory Hitachi Ltd.

• Yoshizawa Junichi

  Computer & Communication Research Center The Tokyo Electric Power Co.

• ITO JUNKO

  Faculty of Pharmacy, Meijo University

関連論文

• 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
• Characterization of an Apoptosis-Inducing Factor in Habu Snake Venom as a Glycyrrhizin (GL)-binding Protein Potently Inhibited by GL in VItro
• 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
• Biochemical Characterization of 60S Acidic Ribosomal P Proteins from Porcine Liver and the Inhibition of Their Immunocomplex Formation with Sera from Systemic Lupus Erythematosus (SLE) Patients by Glycyrrhizin in Vitro
• The Migdal-Kadanoff Transformations on the Dual Lattice : Particles and Fields
• 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 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
• Triterpenoids from the Cork of Vitis vinifera "Kyohou"
• Logic Verification System for Power Plant Sequence Diagrams.
• Approach to knowledge based man-machine communication for BWR start-up guidance.

もっと見る 閉じる

スポンサーリンク