• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Research on Formal Verification of Finite State Systems

Research Project

Project/Area Number 05680285
Research Category

Grant-in-Aid for General Scientific Research (C)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionKyoto Sangyo University

Principal Investigator

HIRAISHI Hiromi  Kyoto Sangyo Univ., Engineering, Professor, 工学部, 教授 (40093299)

Project Period (FY) 1993 – 1994
Project Status Completed (Fiscal Year 1994)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 1994: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1993: ¥1,300,000 (Direct Cost: ¥1,300,000)
KeywordsFormal Design Verification / Finite State Systems / Temporal Logic / Symbolic Model Checking / Logic Design Verification / 設計検証 / 形式的検証 / 分散アルゴリズム / 抽象化
Research Abstract

Aiming at establishment of fundamental formal verification methodology for finite state systems of practical size, I mainly investigated formal design verification based on symbolic model checking of temporal logic. The major results of this research are summarized below :
1.Symbolic Model Checking Algorithm : Since an inverse image computation is one of the basic operations in symbolic model checking of temporal logic, I proposed an efficient new inverse image computation algorithm. The proposed algorithm was applied to a verification of 8 bit microprocessor, and the result showed that the new algorithm achieved around 60 times speed-up compared with conventional inverse image computation algorithms.
2.Time-Space Modal Logic : Aiming at verification of bit-slice architecture, I proposed a new transition system that has tow types of transition ; one for time transitions and the others for space transitions. The transition system cab be used as a model of a bit-slice circuits. As for a specification language on the transition system, I proposed time-space modal logic and showed its symbolic model checking algorithm.
3.Verification of Real-Time Systems : As for basic algorithms in verification of real-time systems, a couple of symbolic algorithms have been proposed. By using these algorithms, we can obtain upper bound and lower bound of time between two types of events and upper bound and lower bound of event occurrences in a given time period. These are basic characteristics of real-time systems and calculations of them are important in verification of real-time systems.
4.Formal Verification of 16 bit microprocessor : Various abstract methods were investigated to make verification of 16 bit microprocessor possible. Among them, abstraction of data width to 8 bit and signal fixing were very effective. By combining these two methods, we succeeded to verify 16 bit microprocessor.

Report

(3 results)
  • 1994 Annual Research Report   Final Research Report Summary
  • 1993 Annual Research Report
  • Research Products

    (17 results)

All Other

All Publications (17 results)

  • [Publications] H. Hiraishi: "Formal Varification of Single Phase Behavior of KUE‐CHIP2 Microprocessor" New Advances in Computer Aided Design & Computer Graphics. 2. 611-616 (1993)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H. Hiraishi: "An Efficient Inverse Image Computation Algorithm for Sequentail Machine Verification" Proc. of Pacific Rim International Symposium on Fault Tolerant Computing. 91-95 (1993)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H. Hiraishi: "An Efficient Inverse Image Computation Algorithm for Sequentail Machine Verification Using Temporal Logics" Computer Systems Science & Engineering. 9. 112-117 (1994)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] 平石裕実: "論理関数処理に基づく形式的検証" 情報処理. 35. 710-718 (1994)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H. Hiraishi: "Time‐Space Modal Model Checking towards Verification of Bit‐Slice Architecture" Proc. of 3rd Asian Test Symposium. 287-291 (1994)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] S. V. Campos: "Computing Quantitative Characteristics of Finite‐State Real‐Time Systems" Proc. of Real‐Time Systems Symposium. 266-270 (1994)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H.Hiraishi: "Formal Verification of Single Phase Behavior of KUECHIP2 Microprocessor" New Advances in Computer Aided Design & Computer Graphics. Vol.II. 611-616 (1993)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H.Hiraishi: "An Efficient Inverse Image Computation Algorithm for Sequential Machine Verification" Proc.Pacific Rim International Symp.on Fault Tolerant Computing. 91-95 (1993)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H.Hiraishi: "An Efficient Inverse Image Computation Algorithm for Sequential Machine Verification Using Temporal Logics" Computer Systems Science & Engineering. Vol.9. 112-117 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H.Hiraishi: "Formal Verification Based on Logic Function Processing" Information Processing. Vol.35. 710-718 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] H.Hiraishi: "Time-Space Modal Model Checking towards Verification of Bit-Slice Architecture" Proc.3rd Asian Test Symp.287-291 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] S.V.Campos, Computing Quantitative Characteristics of Finite-State Real-Time Systems. Proc.Real-Time Systems Symp., 266-270 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1994 Final Research Report Summary
  • [Publications] 平石裕実: "論理関数処理に基づく形式的検証手法" 情報処理. 35. 710-718 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] H.Hiraishi: "Time-Space Modal Model Checking towards Verification of Bit-Slice Architecture" Proc.3rd Asian Test Symp.287-291 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] S.V.Campos: "Computing Quantitative Characteristics of Finite-State Real-Time Systems" Proc.Real-Time System Symp.266-270 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] 平石裕実: "Formal Verification of Single Phase Behavior of KUE-CHIP2 Microprocessor" New Advances in Computer Aided Design Z Computer Graphics. 2. 611-616 (1993)

    • Related Report
      1993 Annual Research Report
  • [Publications] 平石裕実: "An Efficient Inverse Image Computation Algorithm for Seguenfial Machine Verificafion" Proc.PRFTS'93. 91-95 (1993)

    • Related Report
      1993 Annual Research Report

URL: 

Published: 1993-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi