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

2015 Fiscal Year Annual Research Report

証明スコア法に基づく革新的仕様検証システムの構築

Research Project

Project/Area Number 23220002
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

二木 厚吉  北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 特任教授 (50251971)

Co-Investigator(Kenkyū-buntansha) 緒方 和博  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
青木 利晃  北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹  富山県立大学, 工学部, 講師 (40345658)
Project Period (FY) 2011-04-01 – 2016-03-31
Keywords仕様記述・仕様検証 / 形式手法 / 代数仕様 / 証明スコア / 定理証明 / CafeOBJ
Outline of Annual Research Achievements

仕様検証法研究と事例開発を相互補完的に展開しつつ、それらの成果をCafeOBJ仕様言語システムに組み込むことで、革新的仕様検証システムを構築した。
適切な抽象度の実現については,CafeOBJ言語の順序ソート機能を使い観測遷移システム(OTS)の観測子の引数の詳細化を系統的に行う技術と、状態を観測子の集合または列とすることで観測子を必要な詳細度で参照・捨象する技術を整理体系化した。
推論型×探索型検証法については,(i)Generate&Check法を支援する汎用ライブラリをCafeOBJのパラメータ化モジュールとして整理体系化し論文発表するとともに,(ii)構成子に基づく帰納的検証システム(CITP)をCafeOBJ言語システムに組み込み推論型証明支援を実現した。
ソフトウェア自動更新事例については,ソフトウェア自動更新のOTS(観測遷移システム) による形式化とそれに基づく形式検証技術を完成し論文発表した。車載OS標準事例については,車載OS国際標準OSEK/VDX Operating System 2.2.3 (英文86ページの国際標準)のCafeOBJ形式仕様と、それに基づくデッドロックや優先度逆転が発生しないことの形式検証を完成し、その成果をウェッブページを通じて発信した。
上記の成果をCafeOBJ形式仕様言語システムへ統合することで、革新的仕様検証システムを完成し、ホームページ(cafeobj.org)を通じて世界に向けて発信した。

Research Progress Status

27年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

27年度が最終年度であるため、記入しない。

  • Research Products

    (15 results)

All 2016 2015 Other

All Int'l Joint Research (2 results) Journal Article (8 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 8 results,  Open Access: 6 results,  Acknowledgement Compliant: 6 results) Presentation (2 results) (of which Int'l Joint Research: 2 results,  Invited: 1 results) Remarks (1 results) Funded Workshop (2 results)

  • [Int'l Joint Research] マドリッド大学 (UCM)(スペイン)

    • Country Name
      SPAIN
    • Counterpart Institution
      マドリッド大学 (UCM)
  • [Int'l Joint Research] 華東師範大学(中国)

    • Country Name
      CHINA
    • Counterpart Institution
      華東師範大学
  • [Journal Article] CafeInMaude: A CafeOBJ Interpreter in Maude2016

    • Author(s)
      Adrian Riesco, Kazuhiro Ogata, Kokichi Futatsugi
    • Journal Title

      Springer Lecture Notes in Computer Science (Fundamental Approaches to Software Engineering, 19th FASE)

      Volume: 9633 Pages: 377-380

    • DOI

      10.1007/978-3-662-49665-7_22

    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Generic Proof Scores for Generate & Check Method in CafeOBJ2015

    • Author(s)
      Kokichi Futatsugi
    • Journal Title

      Springer LNCS (Logic, Rewriting, and Concurrency)

      Volume: 9200 Pages: 287-310

    • DOI

      10.1007/978-3-319-23165-5_14

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Formalization and Verification of Declarative Cloud Orchestration2015

    • Author(s)
      Hiroyuki Yoshida, Kokichi Futatsugi, Kazuhiro Ogata
    • Journal Title

      Springer Lecture Note in Computer Science (Formal Methods and Software Engineering, 17th ICFEM)

      Volume: 9407 Pages: 33-49

    • DOI

      10.1007/978-3-319-25423-4_3

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates2015

    • Author(s)
      Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
    • Journal Title

      Proc. of 22nd Asia-Pacific Software Engineering Conference

      Volume: - Pages: -

    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Proving Sufficient Completeness of Constructor-based Algebraic Specifications2015

    • Author(s)
      Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata and Kokichi Futatsugi
    • Journal Title

      Springer Lecture Notes in Electrical Engineering (Advances in Computer Science and Ubiquitous Computing)

      Volume: 373 Pages: 15-21

    • DOI

      10.1007/978-981-10-0281-6_3

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Foundations of Logic Programming in Hybridised Logics2015

    • Author(s)
      Daniel Gaina
    • Journal Title

      Springer Lecture Notes in Computer Science (Recent Trends in Algebraic Development Techniques)

      Volume: 9463 Pages: 69-89

    • DOI

      10.1007/978-3-319-28114-8_5

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] A Framework for Verifying the Conformance of Design to Its Formal Specifications2015

    • Author(s)
      Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
    • Journal Title

      IEICE Transactions

      Volume: E98-D-6 Pages: 1137-1149

    • DOI

      10.1587/transinf.2014FOP0004

    • Peer Reviewed
  • [Journal Article] Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach2015

    • Author(s)
      Haitao Zhang, Toshiaki Aoki, Yuki Chiba
    • Journal Title

      IEICE Transactions

      Volume: E98-D-10 Pages: 1765-1776

    • DOI

      10.1587/transinf.2015EDP7043

    • Peer Reviewed
  • [Presentation] Recent Developments on Algebraic Specification and Verification in CafeOBJ2015

    • Author(s)
      Kokichi Futatsugi
    • Organizer
      2nd International Symposium on Dependable Computing and Internet of Things (DICT 2015)
    • Place of Presentation
      Wuhan, China
    • Year and Date
      2015-11-16 – 2015-11-18
    • Int'l Joint Research / Invited
  • [Presentation] Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications2015

    • Author(s)
      Haitao Zhang, Toshiaki Aoki, Yuki Chiba
    • Organizer
      IEEE International Conference on Software Testing, Verification and Validation
    • Place of Presentation
      Graz, Austria
    • Year and Date
      2015-04-13 – 2015-04-17
    • Int'l Joint Research
  • [Remarks] CafeOBJ - Algebraic Specification and Verification

    • URL

      https://cafeobj.org

  • [Funded Workshop] JAIST Mathematical Logic and Software Verification Joint Workshop2015

    • Place of Presentation
      Hotel Arrowle, Kaga-shi, Ishikawa, JAPAN
    • Year and Date
      2015-12-03 – 2015-12-04
  • [Funded Workshop] JAIST Software Verification Research Center Workshop2015

    • Place of Presentation
      Hotel Arrowle, Kaga-shi, Ishikawa, JAPAN
    • Year and Date
      2015-06-25 – 2015-06-26

URL: 

Published: 2017-01-06  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi