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

2004 Fiscal Year Final Research Report Summary

Research on an efficient analysis method of real-time software based on a level oriented net model

Research Project

Project/Area Number 15300009
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field Software
Research InstitutionNational Institute of Informatics

Principal Investigator

YONEDA Tomohiro  National Institute of Informatics, Infrastructure Systems Research Division, Professor, 情報基盤研究系, 教授 (30182851)

Project Period (FY) 2003 – 2004
KeywordsLevel Time Petri net / Partial order reduction / Hierarchical verification / Real time software / Timed automaton
Research Abstract

It is well known that a timed automaton is a formal model for real-time systems which is level oriented and has rich expressiveness. Our experience, however, has found that its generality comes at an increase in analysis complexity, and this increased generality is not always necessary for verifying some class of real-time, systems. Thus, this work has tackled the challenge to develop an efficient tool based on a simpler model with still sufficient expressiveness.
In the first step of this work, a new formal model has been obtained by extending the time Petri net model with preserving the simplicity of its analysis. In this new model called LTN (Level Time Petri net), firing an LTN transition can assign values to a set of boolean variables, and the validity of an expression over the boolean variables is also used as an enabling condition of an LTN transition in addition to the marking. Next, its efficient analysis procedure based on the partial order reduction has been developed and an prototype for it has been implemented. This algorithm also has an ability of verifying systems hierarchically, which sometimes reduces the average complexity of the verification of large systems. To demonstrate this ability, a little large case study for verifying the instruction cache mechanism of TITAC 2 asynchronous microprocessor has been done. Through the case study, the hierarchical verification technique has been evaluated. Finally, we have designed a graphical user interface (GUI) for especially supporting the hierarchical verification steps, and a verification tool VINAS-P(Ver.2) with it has been developed.

  • Research Products

    (6 results)

All 2003 Other

All Journal Article (6 results)

  • [Journal Article] Partial Order Reduction for Timed Circuit Verification Based on a Level Oriented Model2003

    • Author(s)
      Tomoya Kitai
    • Journal Title

      電子情報通信学会英文論文誌 Vol.E86-D

      Pages: 2601-2611

    • Description
      「研究成果報告書概要(和文)」より
  • [Journal Article] Partial Order Reduction for Timed Circuit Verification Based on a Level Oriented Model2003

    • Author(s)
      Tomoya Kitai, Yusuke Oguro, Tomohiro Yoneda, Eric Mercer, Chris Myers
    • Journal Title

      Proc. of IEICE Vol.E86-D No.12

      Pages: 2601-2611

    • Description
      「研究成果報告書概要(欧文)」より
  • [Journal Article] Partial order Reduction for Detecting Safety and Timing Failures of Timed Circuits

    • Author(s)
      Denduang Pradubsuwun
    • Journal Title

      電子情報通信学会英文論文誌 (印刷中)

    • Description
      「研究成果報告書概要(和文)」より
  • [Journal Article] Failure Trace analysis of Timed Circuits for Automatic Timing Constraints Derivation

    • Author(s)
      Tomoya Kitai
    • Journal Title

      電子情報通信学会英文論文誌 (印刷中)

    • Description
      「研究成果報告書概要(和文)」より
  • [Journal Article] Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits

    • Author(s)
      Denduang Pradubsuwun, Tomohiro Yoneda, Chris Myers
    • Journal Title

      Proc. of IEICE (to appear)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Journal Article] Failure Trace analysis of Timed Circuits for Automatic Timing Constraints Derivation

    • Author(s)
      Tomoya Kitai, Tomohiro Yoneda, Chris Myers
    • Journal Title

      Proc. of IEICE (to appear)

    • Description
      「研究成果報告書概要(欧文)」より

URL: 

Published: 2006-07-11  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi