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

Reuse of Abstraction in Model Checking

Research Project

Project/Area Number 20700004
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionTottori University of Environmental Studies

Principal Investigator

NISHIZAWA Koki  Tottori University of Environmental Studies, 環境情報学部, 講師 (60455433)

Project Period (FY) 2008 – 2009
Project Status Completed (Fiscal Year 2009)
Budget Amount *help
¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2009: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2008: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywords情報基礎 / システム検証 / モデル検査 / 抽象化 / 多値論理
Research Abstract

There is no end to the number of problem posed by bugs of software and hardware. Model checking is the technique to verify such systems. We gives a theory to reuse'abstraction' that is efficiency technology in model checking. The cost of abstraction is high, because even if an abstraction is efficient to verify a property, it may be inefficient to verify other properties. If this result allows us to reuse abstractions, it reduces the cost of abstractions. We especially gives a theory to reuse abstractions between different multi-valued logics. The validity of abstractions is mathematically guaranteed by using theories about multi-valued logics and simulations.
The results are as follows. We give a general fixed point logic including four multi-valued logics (Frame, De Morgan Frame, Bilattice, Mied TS) as examples. Under the logic, we formulate abstractions by using `the pair of two adjunctions'and prove that the abstraction allows us to pull back results of verification. Moreover, we give the sufficient condition to reuse such abstractions.
As related work, we also analyze unary operators on multi-valued logics whose truth values form a powerset. We discover the correspondence between the hierarchy of Kleene algebras and the hierarchy of multirelations that is another representation of such unary operators.

Report

(3 results)
  • 2009 Annual Research Report   Final Research Report ( PDF )
  • 2008 Annual Research Report
  • Research Products

    (11 results)

All 2009 2008 Other

All Journal Article (8 results) (of which Peer Reviewed: 8 results) Presentation (3 results)

  • [Journal Article] An algebraic semantics of predicate abstraction for PML2009

    • Author(s)
      Y. Kinoshita, K. Nishizawa
    • Journal Title

      コンピュータソフトウェア Vol.26、No.2

      Pages: 147-156

    • NAID

      130004892130

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Multirelational Models of Lazy, Monodic Tree, and Probabilistic Kleene Algebras2009

    • Author(s)
      H. Furusawa, K. Nishizawa, N. Tsumagari
    • Journal Title

      Bulletin of Informatics and Cybernetics Vol.41

      Pages: 40871-40871

    • NAID

      120003878376

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] The cube of Kleene algebras and the triangular prism of multirelations2009

    • Author(s)
      K. Nishizawa、N. Tsumagari、H. Furusawa
    • Journal Title

      Relations and Kleene Algebra in Computer Science RelMiCS/AKA(Springer LNCS) Vol.5827

      Pages: 276-290

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] The cube of Kleene algebras and the triangular prism of multirelations2009

    • Author(s)
      K.Nishizawa, N.Tsumagari, H.Furusawa
    • Journal Title

      Relations and Kleene Algebra in Computer Science RelMiCS/AKA(Springer LNCS) 5827

      Pages: 276-290

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] An algebraic semantics of predicate abstraction for PML2009

    • Author(s)
      Y. Kinoshita and K. Nishizawa
    • Journal Title

      コンピュータソフトウェア Vol.26, No.2

      Pages: 147-156

    • NAID

      130004892130

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Non-Probabilistic Relational Model of Probabilistic Kleene Algebras2008

    • Author(s)
      H. Furusawa, N. Tsumagari, K Nishizawa
    • Journal Title

      Proc. Relations and Kleene Algebra in Computer Science, LNCS Vol.4988

      Pages: 110-122

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] A Non-Probabilistic Relational Model of Probabilistic Kleene Algebras2008

    • Author(s)
      H. Furusawa, N. Tsumagari, K Nishizawa
    • Journal Title

      Proc. Relations and Kleene Algebra in Computer Science, LNCS 4988

      Pages: 110-122

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Multirelational Models of Lazy, Monodic Tree, and Probabilistic Kleene Algebras

    • Author(s)
      H. Furusawa, K. Nishizawa, N. Tsumagari
    • Journal Title

      Bulletin of Informatics and Cybernetics (掲載予定)

    • NAID

      120003878376

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Presentation] Multi-valued modal fixed point logics for model checking2009

    • Author(s)
      K. Nishizawa
    • Organizer
      39th International Symposium on Multiple-Valued Logics
    • Place of Presentation
      沖縄産業支援センター(招待講演)
    • Year and Date
      2009-05-21
    • Related Report
      2009 Final Research Report
  • [Presentation] Multi-valued modal fixed point logics for model checking2009

    • Author(s)
      K.Nishizawa
    • Organizer
      39^<th> International Symposium on Multiple-Valued Logics
    • Place of Presentation
      沖縄産業支援センター(那覇市)
    • Year and Date
      2009-05-21
    • Related Report
      2009 Annual Research Report
  • [Presentation] 二項多重関係の反射的推移的閉包2008

    • Author(s)
      津曲紀宏, 西澤弘毅, 古澤仁
    • Organizer
      日本ソフトウェア科学会25回大会
    • Place of Presentation
      筑波大学
    • Year and Date
      2008-09-11
    • Related Report
      2009 Final Research Report 2008 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi