• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

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

研究課題

研究課題/領域番号 23220002
研究種目

基盤研究(S)

配分区分補助金
研究分野 ソフトウエア
研究機関北陸先端科学技術大学院大学

研究代表者

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

研究分担者 緒方 和博  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
青木 利晃  北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹  富山県立大学, 工学部, 講師 (40345658)
連携研究者 千葉 勇輝  北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
清野 貴博  産業技術総合研究所, 社会知能研究ラボ, 特別研究員 (10397226)
研究協力者 PREINING Norbert  北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 准教授 (60571247)
GAINA Daniel  北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 助教 (80595778)
研究期間 (年度) 2011-04-01 – 2016-03-31
研究課題ステータス 完了 (2015年度)
配分額 *注記
174,590千円 (直接経費: 134,300千円、間接経費: 40,290千円)
2015年度: 35,880千円 (直接経費: 27,600千円、間接経費: 8,280千円)
2014年度: 37,050千円 (直接経費: 28,500千円、間接経費: 8,550千円)
2013年度: 37,570千円 (直接経費: 28,900千円、間接経費: 8,670千円)
2012年度: 37,050千円 (直接経費: 28,500千円、間接経費: 8,550千円)
2011年度: 27,040千円 (直接経費: 20,800千円、間接経費: 6,240千円)
キーワード仕様記述・仕様検証 / 形式手法 / ソフトウェア工学 / 代数仕様 / 証明スコア / CafeOBJ / 定理証明
研究成果の概要

仕様検証法の最重要課題として(1)適切な抽象度と(2)推論型×探索型検証を実現する技術の研究を、重要な仕様検証事例として(3)ソフトウェア自動更新と(4)車載OS標準の事例開発を、補完的に推進した。(1)-(4)の成果を、CafeOBJ仕様言語システムに統合することで、革新的仕様検証システムを実現した。本研究の成果である[革新的仕様検証システム=最新版CafeOBJ仕様言語システム]はホームページ(cafeobj.org)を通じてフリーウェアとして入手可能であり、UNIX/Linux, MacOS, Windowsの3つの主要なプラットホームで実行可能である。

評価記号
検証結果 (区分)

A

評価記号
評価結果 (区分)

A: 当初目標に向けて順調に研究が進展しており、期待どおりの成果が見込まれる

報告書

(9件)
  • 2016 研究進捗評価(検証) ( PDF )
  • 2015 実績報告書   研究成果報告書 ( PDF )
  • 2014 実績報告書   研究概要(研究進捗評価) ( PDF )   研究進捗評価(評価結果) ( PDF )
  • 2013 実績報告書
  • 2012 実績報告書
  • 2011 実績報告書
  • 研究成果

    (90件)

すべて 2016 2015 2014 2013 2012 2011 その他

すべて 国際共同研究 (2件) 雑誌論文 (66件) (うち国際共著 2件、 査読あり 64件、 オープンアクセス 6件、 謝辞記載あり 18件) 学会発表 (11件) (うち国際学会 2件、 招待講演 5件) 図書 (2件) 備考 (7件) 学会・シンポジウム開催 (2件)

  • [国際共同研究] マドリッド大学 (UCM)(スペイン)

    • 関連する報告書
      2015 実績報告書
  • [国際共同研究] 華東師範大学(中国)

    • 関連する報告書
      2015 実績報告書
  • [雑誌論文] CafeInMaude: A CafeOBJ Interpreter in Maude2016

    • 著者名/発表者名
      Adrian Riesco, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

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

      巻: 9633 ページ: 377-380

    • DOI

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

    • ISBN
      9783662496640, 9783662496657
    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [雑誌論文] Generic Proof Scores for Generate & Check Method in CafeOBJ2015

    • 著者名/発表者名
      Kokichi Futatsugi
    • 雑誌名

      Springer LNCS (Logic, Rewriting, and Concurrency)

      巻: 9200 ページ: 287-310

    • DOI

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

    • ISBN
      9783319231648, 9783319231655
    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] Formalization and Verification of Declarative Cloud Orchestration2015

    • 著者名/発表者名
      Hiroyuki Yoshida, Kokichi Futatsugi, Kazuhiro Ogata
    • 雑誌名

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

      巻: 9407 ページ: 33-49

    • DOI

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

    • ISBN
      9783319254227, 9783319254234
    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates2015

    • 著者名/発表者名
      Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proc. of 22nd Asia-Pacific Software Engineering Conference

      巻: -

    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [雑誌論文] Proving Sufficient Completeness of Constructor-based Algebraic Specifications2015

    • 著者名/発表者名
      Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata and Kokichi Futatsugi
    • 雑誌名

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

      巻: 373 ページ: 15-21

    • DOI

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

    • ISBN
      9789811002809, 9789811002816
    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] Foundations of Logic Programming in Hybridised Logics2015

    • 著者名/発表者名
      Daniel Gaina
    • 雑誌名

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

      巻: 9463 ページ: 69-89

    • DOI

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

    • ISBN
      9783319281131, 9783319281148
    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] A Framework for Verifying the Conformance of Design to Its Formal Specifications2015

    • 著者名/発表者名
      Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: E98.D 号: 6 ページ: 1137-1149

    • DOI

      10.1587/transinf.2014FOP0004

    • NAID

      130005072395

    • ISSN
      0916-8532, 1745-1361
    • 関連する報告書
      2015 実績報告書
    • 査読あり
  • [雑誌論文] Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach2015

    • 著者名/発表者名
      Haitao Zhang, Toshiaki Aoki, Yuki Chiba
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: E98.D 号: 10 ページ: 1765-1776

    • DOI

      10.1587/transinf.2015EDP7043

    • NAID

      130005101306

    • ISSN
      0916-8532, 1745-1361
    • 関連する報告書
      2015 実績報告書
    • 査読あり
  • [雑誌論文] Generate & Check Method for Verifying Transition Systems in CafeOBJ2015

    • 著者名/発表者名
      Kokichi Futatsugi
    • 雑誌名

      Software, Services, and Systems, LNCS, Springer

      巻: 8950 ページ: 171-192

    • DOI

      10.1007/978-3-319-15545-6_13

    • ISBN
      9783319155449, 9783319155456
    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Initial semantics in logics with constructors2015

    • 著者名/発表者名
      Daniel Gaina, Kokichi Futatsugi
    • 雑誌名

      Journal of Logic and Computation

      巻: 25 (1) 号: 1 ページ: 95-116

    • DOI

      10.1093/logcom/exs044

    • 関連する報告書
      2014 実績報告書
    • 査読あり
  • [雑誌論文] 構成子に基づく順序ソートパラメータ化仕様の十分完全性について2015

    • 著者名/発表者名
      中村正樹,ガイナ ダニエル ミルチェア,緒方和博,二木厚吉
    • 雑誌名

      電子情報通信学会,信学技報

      巻: vol.114, no.510, SS2014-55 ページ: 1-6

    • 関連する報告書
      2014 実績報告書
    • 謝辞記載あり
  • [雑誌論文] TESLA source authentication protocol verification experiment in the Timed OTS/CafeOBJ method: Experiences and Lessons Learned2014

    • 著者名/発表者名
      Iakovos Ouranos, Petros Stefaneas, Kazuhiro Ogata
    • 雑誌名

      IEICE TRANSACTIONS on Information and Systems

      巻: E97-D(5) ページ: 1160-1170

    • NAID

      130004519231

    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] A Formal Semantics of the OSEK/VDX Standard in K Framework and its Applications2014

    • 著者名/発表者名
      Min Zhang, Yunja Choi, Kazuhiro Ogata
    • 雑誌名

      Pro. of 10th RTA, LNCS, Springer

      巻: 8663 ページ: 280-296

    • DOI

      10.1007/978-3-319-12904-4_16

    • ISBN
      9783319129037, 9783319129044
    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs2014

    • 著者名/発表者名
      Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Specification, Algebra, and Software, LNCS, Springer

      巻: 8373 ページ: 630-656

    • DOI

      10.1007/978-3-642-54624-2_31

    • ISBN
      9783642546235, 9783642546242
    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Evaluation of Maude as a test generation engine for automotive operating systems2014

    • 著者名/発表者名
      Yunja Choi, Min Zhang, Kazuhiro Ogata
    • 雑誌名

      Proc. of the 21st Asia-Pacific Software Engineering Conference (21st APSEC), IEEE

      巻: -

    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Checking the Conformance of a Promela Design to Its Formal Specification in Event-B2014

    • 著者名/発表者名
      Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
    • 雑誌名

      Proc. of 3rd Intl. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)

      巻: - ページ: 203-218

    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] A Spin-based Approach for Checking OSEK/VDX Applications2014

    • 著者名/発表者名
      Haitao Zhang, Toshiaki Aoki, and Yuki Chiba
    • 雑誌名

      Proc. of 3rd Intl. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)

      巻: - ページ: 187-202

    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications2014

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Specification, Algebra, and Software, LNCS, Springer

      巻: 8373 ページ: 92-109

    • DOI

      10.1007/978-3-642-54624-2_5

    • ISBN
      9783642546235, 9783642546242
    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] An incremental approach to local equality predicates in OBJ specification languages2014

    • 著者名/発表者名
      Masaki Nakamura, Kokichi Futatsugi
    • 雑誌名

      Proc. of Intl. Joint Conference on Computer Science and Software Engineering (11th JCSSE), IEEE

      巻: - ページ: 337-342

    • DOI

      10.1109/jcsse.2014.6841891

    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences2014

    • 著者名/発表者名
      Arnold Beckmann, Norbert Preining
    • 雑誌名

      Journal of Logic and Computation

      巻: - 号: 3 ページ: 527-547

    • DOI

      10.1093/logcom/exu016

    • NAID

      120005625736

    • 関連する報告書
      2014 実績報告書
    • 査読あり
  • [雑誌論文] Liveness properties in CafeOBJ - a case study for meta-level specifications2014

    • 著者名/発表者名
      Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Technical Report IASI-CNR R. 3, 2014, ISSN: 1128-3378

      巻: -

    • 関連する報告書
      2014 実績報告書
    • 謝辞記載あり
  • [雑誌論文] On Automation of OTS/CafeOBJ Method2014

    • 著者名/発表者名
      Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Specification, Algebra, and Software, LNCS, Springer

      巻: 8373 ページ: 578-602

    • DOI

      10.1007/978-3-642-54624-2_29

    • ISBN
      9783642546235, 9783642546242
    • 関連する報告書
      2014 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Forcing, Downward Lowenheim-Skolem and Omitting Types Theorems, Institutionally2014

    • 著者名/発表者名
      Daniel Gaina
    • 雑誌名

      Logica Universalis

      巻: 8 (3-4) 号: 3-4 ページ: 469-498

    • DOI

      10.1007/s11787-013-0090-0

    • 関連する報告書
      2014 実績報告書
    • 査読あり
  • [雑誌論文] Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method2013

    • 著者名/発表者名
      Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      The Journal of Universal Computer Science (J. UCS)

      巻: 19(6) ページ: 771-804

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions2013

    • 著者名/発表者名
      Kazuhiro Ogata
    • 雑誌名

      Proc. of the 20th Asia-Pacific Software Engineering Conference (20th APSEC), IEEE

      巻: - ページ: 565-570

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] A Divide & Conquer Approach to Model Checking of Liveness Properties2013

    • 著者名/発表者名
      Kazuhiro Ogata, Min Zhang
    • 雑誌名

      Proc. of the 37th Annual International Computer Software & Applications Conference (37th COMPSAC), IEEE Computer Society Press

      巻: - ページ: 648-657

    • DOI

      10.1109/compsac.2013.104

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Formalization and Verification of Behavioral Correctness of Dynamic Software Updates2013

    • 著者名/発表者名
      Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proc. of the 2nd Workshop on Validation Strategies for Software Evolution (2nd VSSE), ENTCS 294, Elsevier

      巻: - ページ: 12-23

    • DOI

      10.1016/j.entcs.2013.02.013

    • NAID

      120005469624

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Constructor-Based Inductive Theorem Prover2013

    • 著者名/発表者名
      Daniel Gaina, Min Zhang, Yuki Chiba, Yasuhito Arimoto
    • 雑誌名

      Proc. of the 5th International Conference on Algebra and Coalgebra in Computer Science (5th CALCO), LNCS 8089, Springer

      巻: - ページ: 328-333

    • DOI

      10.1007/978-3-642-40206-7_26

    • ISBN
      9783642402050, 9783642402067
    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs2013

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      IAENG International Journal of Computer Science

      巻: 40-2 ページ: 117-123

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Active Learning of Nondeterministic Finite State Machines2013

    • 著者名/発表者名
      Warawoot Pacharoen, Toshiaki Aoki, Pattarasinee Bhattarakosol, Athasit Surarerks
    • 雑誌名

      Mathematical Problems in Engineering 2013

      巻: Article ID 373265 ページ: 1-11

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] SMT-based Bounded Model Checking for OSEK/VDX Applications2013

    • 著者名/発表者名
      Haitao Zhang, Toshiaki Aoki, Hsin-Hung Lin, Min Zhang, Yuki Chiba, Kenro Yatake
    • 雑誌名

      Proc. of 20th Asia-Pacific Software Engineering Conference(APSEC)

      巻: - ページ: 307-314

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Preserving correctness of requirements evolution through refinement in Event-B2013

    • 著者名/発表者名
      Kriangkrai Traichaiyaporn, Toshiaki Aoki
    • 雑誌名

      Proc. of 20th Asia-Pacific Software Engineering Conference (APSEC)

      巻: - ページ: 315-322

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] A Practical Study of Debugging using Model Checking2013

    • 著者名/発表者名
      Hideto Ogawa, Makoto Ichii, Fumihiko Kumeno and Toshiaki Aoki
    • 雑誌名

      Proc. of 20th Asia-Pacific Software Engineering Conference (APSEC)

      巻: - ページ: 134-139

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] An approach for checking OSEK/VDX applications2013

    • 著者名/発表者名
      Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang and Hsin-Hung Lin
    • 雑誌名

      Proc. of the 13th International Conference on Quality Software (QSIC)

      巻: - ページ: 113-116

    • DOI

      10.1109/qsic.2013.62

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Building A Body of Knowledge on Model Checking for Software Development2013

    • 著者名/発表者名
      Kenji Taguchi, Hideaki Nishihara, Toshiaki Aoki, Fumihiro Kumeno, Koji Hayamizu, Koichi Sinozaki
    • 雑誌名

      Proc. of the 37th Annual International Computer Software & Applications Conference (37th COMPSAC), IEEE Computer Society Press

      巻: - ページ: 784-789

    • DOI

      10.1109/compsac.2013.129

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Towards Formal Description of Standards for Automotive Operating Systems2013

    • 著者名/発表者名
      Hirokazu Yatsu, Takahiro Ando, Weiqiang Kong, Kenji Hisazumi, Akira Fukuda, Toshiaki Aoki, Kokichi Futatsugi
    • 雑誌名

      ICST Workshops

      巻: - ページ: 13-14

    • DOI

      10.1109/icstw.2013.8

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Refinement Tree and Its Patterns: a Graphical Approach for Event-B Modeling2013

    • 著者名/発表者名
      Kriangkrai Traichaiyaporn, Toshiaki Aoki
    • 雑誌名

      Proc. of Second International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)

      巻: - ページ: 246-261

    • DOI

      10.1007/978-3-319-05416-2_16

    • ISBN
      9783319054155, 9783319054162
    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol2013

    • 著者名/発表者名
      Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake, Toshiaki Aoki
    • 雑誌名

      Proc. of Second International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)

      巻: - ページ: 36-53

    • DOI

      10.1007/978-3-319-05416-2_4

    • ISBN
      9783319054155, 9783319054162
    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Interpolation in logics with constructors2013

    • 著者名/発表者名
      Daniel Gaina
    • 雑誌名

      Theoretical Computer Science (TCS)

      巻: 474 ページ: 46-59

    • DOI

      10.1016/j.tcs.2012.12.002

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Evaluation of Operational Vulnerability in Cloud Service Management using Model Checking2013

    • 著者名/発表者名
      Shinji Kikuchi, Toshiaki Aoki
    • 雑誌名

      Proc. of IEEE Seventh International Symposium on Service-Oriented System Engineering (SOSE)

      巻: - ページ: 37-48

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs2013

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proceedings of the International MultiConference of Engineers and Computer Scientists 2013

      巻: I, IMECS ページ: 516-521

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] A Hierarchical Approach to Operational Termination of Algebraic Specifications2013

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proceedings of the International Conference on Electronics, Information and Communication (ICEIC 2013)

      巻: - ページ: 144-145

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Principles of proof scores in CafeOBJ2012

    • 著者名/発表者名
      Kokichi Futatsugi, Daniel Gaina, Kazuhiro Ogata
    • 雑誌名

      Theoretical Computer Science (TCS)

      巻: 464 ページ: 90-112

    • DOI

      10.1016/j.tcs.2012.07.041

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Constructor-based Logics2012

    • 著者名/発表者名
      Daniel Gaina, Kokichi Futatsugi, Kazuhiro Ogata
    • 雑誌名

      The Journal of Universal Computer Science (J.UCS)

      巻: 18(16) ページ: 2204-2233

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification2012

    • 著者名/発表者名
      Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
    • 雑誌名

      IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

      巻: E95.A 号: 9 ページ: 1451-1460

    • DOI

      10.1587/transfun.E95.A.1451

    • NAID

      10031142529

    • ISSN
      0916-8508, 1745-1337
    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking2012

    • 著者名/発表者名
      Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: E95.D 号: 7 ページ: 1882-1893

    • DOI

      10.1587/transinf.E95.D.1882

    • NAID

      10031024282

    • ISSN
      0916-8532, 1745-1361
    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method2012

    • 著者名/発表者名
      Iakovos Ouranos, Petros S. Stefaneas, Kazuhiro Ogata
    • 雑誌名

      Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (5th ISoLA), Part I

      巻: Springer LNCS 7610 ページ: 126-142

    • DOI

      10.1007/978-3-642-34032-1_15

    • ISBN
      9783642340314, 9783642340321
    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic2012

    • 著者名/発表者名
      Kazuhiro Ogata, Phan Thi Thanh Huyen
    • 雑誌名

      Proceedings of the 14th International Conference on Formal Engineering Methods (14th ICFEM)

      巻: Springer LNCS 7635 ページ: 87-102

    • DOI

      10.1007/978-3-642-34281-3_9

    • ISBN
      9783642342806, 9783642342813
    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] A Variability Management Method for Software Configuration Files2012

    • 著者名/発表者名
      Hiroaki Tanizaki, Toshiaki Aoki, Takuya Katayama
    • 雑誌名

      Proc. of 24th International Conference on Software Engineering and Knowledge Engineering (SEKE 2012)

      巻: - ページ: 672-677

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Faithfully Formalizing OSEK/VDX Operating System Specification2012

    • 著者名/発表者名
      Dieu-Huong Vu, Toshiaki Aoki
    • 雑誌名

      Proc. of third International Symposium on Information and Communication Technology (SoICT 2012)

      巻: - ページ: 13-20

    • DOI

      10.1145/2350716.2350721

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling2012

    • 著者名/発表者名
      Kenro Yatake, Toshiaki Aoki
    • 雑誌名

      Proc. of International Colloquium on Theoretical Aspect of Computing (ICTAC)

      巻: - ページ: 183-197

    • DOI

      10.1007/978-3-642-32943-2_15

    • ISBN
      9783642329425, 9783642329432
    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules2012

    • 著者名/発表者名
      Min Zhang, Kazuhiro Ogata
    • 雑誌名

      Proceedings of the 19th Asia-Pacific Software Engineering Conference (19th APSEC), IEEE

      巻: - ページ: 511-516

    • DOI

      10.1109/apsec.2012.99

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms2012

    • 著者名/発表者名
      Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proceedings of the 19th Asia-Pacific Software Engineering Conference (19th APSEC), IEEE

      巻: - ページ: 664-673

    • DOI

      10.1109/apsec.2012.100

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] モデル検査とテストによる車載オペレー ティングシステムのシームレスな検証2012

    • 著者名/発表者名
      青木利晃, 佐藤信, 谷充弘, 矢竹健朗
    • 雑誌名

      組込みシステムシンポジウム論文集

      巻: -

    • NAID

      170000072430

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] モデル検査ツールにより出力された反例に基づく誤り特定手法2012

    • 著者名/発表者名
      陳適, 青木利晃
    • 雑誌名

      日本ソフトウェア科学会 ソフトウェア工学の基礎ワークショップ論文集

      巻: - ページ: 27-32

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] UMLに基づくRTOS設計検証のための環境自動生成法2012

    • 著者名/発表者名
      矢竹健朗, 青木利晃
    • 雑誌名

      日本ソフトウェア科学会 学会誌 コンピュータソフトウェア

      巻: 29-3 ページ: 121-142

    • NAID

      130004549272

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Formalization of Risks and Control Activities in Business Process2012

    • 著者名/発表者名
      Yasuhito Arimoto, Shusaku Iida, Kokichi Futatsugi
    • 雑誌名

      Springer Lecture Notes in Electrical Engineering

      ページ: 565-575

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification2012

    • 著者名/発表者名
      Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
    • 雑誌名

      Proc.of 9th IEEE-RIVF International Conference on Computing and Communication Technologies (RIVF 2012)

      ページ: 1-6

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] Facilitating the Transformation of State Machines from Equations into Rewrite Rules2012

    • 著者名/発表者名
      Min Zhang, Kazuhiro Ogata
    • 雑誌名

      Pre-Proceedings of WRLA 2012

      ページ: 183-198

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] On Describing Terminating Algebraic Specifications Based on Their Models2012

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proc.of the International MultiConference of Engineers and Computer Scientists 2012

      ページ: 269-274

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"2011

    • 著者名/発表者名
      Yuan Li, Haibin Kan, Kokichi Futatsugi
    • 雑誌名

      IEICE Transactions

      巻: 94-A(9) ページ: 1877-1880

    • NAID

      10030190955

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support2011

    • 著者名/発表者名
      Min Zhang, Kazuhiro Ogata, Masaki Nakamura
    • 雑誌名

      IEICE TRANSACTIONS on Information and Systems

      巻: E94-D(5) ページ: 976-988

    • NAID

      10029506958

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] A Modeling Framework to Support Internal Control2011

    • 著者名/発表者名
      Takafumi Komoto, Kenji Taguchi, Haralambos Mouratidis, Nobukazu Yoshioka, Kokichi Futatsugi
    • 雑誌名

      Proc.of The Fifth International Conference on Secure Software Integration and Reliability Improvement (IEEE SSIRI 2011)

      ページ: 187-193

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] Conformance Testing for OSEK/VDX Operating System Using Model Checking2011

    • 著者名/発表者名
      Jiang Chen, Toshiaki Aoki
    • 雑誌名

      Proc.of 18th Asia-Pacific Software Engineering Conference (APSEC 2011)

      ページ: 274-281

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] Conformance Verification between Web Service Choreography and Implementation Using Learning and Model Checking2011

    • 著者名/発表者名
      Warawoot Pacharoen, Toshiaki Aoki, Athasit Surarerks, Pattarasinee Bhattarakosol
    • 雑誌名

      Proc.of IEEE International Conference on Web Services (ICWS 2011)

      ページ: 722-723

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] Automated Adaptor Generation for Services Based on Pushdown Model Checking2011

    • 著者名/発表者名
      Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
    • 雑誌名

      Proc.of 18th IEEE International Conference and Workshops on Engineering of Computer-Based Systems (ECBS 2011)

      ページ: 130-139

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [学会発表] Recent Developments on Algebraic Specification and Verification in CafeOBJ2015

    • 著者名/発表者名
      Kokichi Futatsugi
    • 学会等名
      2nd International Symposium on Dependable Computing and Internet of Things (DICT 2015)
    • 発表場所
      Wuhan, China
    • 年月日
      2015-11-16
    • 関連する報告書
      2015 実績報告書
    • 国際学会 / 招待講演
  • [学会発表] Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications2015

    • 著者名/発表者名
      Haitao Zhang, Toshiaki Aoki, Yuki Chiba
    • 学会等名
      IEEE International Conference on Software Testing, Verification and Validation
    • 発表場所
      Graz, Austria
    • 年月日
      2015-04-13
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Large scale testing using computer clusters2015

    • 著者名/発表者名
      Toshiaki Aoki
    • 学会等名
      Static Analysis meets Runtime Verification, Shonan Meeting
    • 発表場所
      Shonan Villlage Center, Hayama, Kanagawa
    • 年月日
      2015-03-16 – 2015-03-19
    • 関連する報告書
      2014 実績報告書
    • 招待講演
  • [学会発表] 車載オペレーティン グシステムを対象としたモデル検査とテストによる正しさの確信手法2014

    • 著者名/発表者名
      青木 利晃, 佐藤 信, 谷 充弘 , 矢竹 健朗, 岸 知二
    • 学会等名
      第21回ソフトウェア工学の基礎ワークショップ
    • 発表場所
      霧島国際ホテル、鹿児島県霧島市
    • 年月日
      2014-12-11 – 2014-12-13
    • 関連する報告書
      2014 実績報告書
  • [学会発表] ISO26262における 安全仕様のゴール木を用いた浅い形式化2014

    • 著者名/発表者名
      青木 利晃,千葉 勇輝,松原 正裕,西 昌能,成沢 文雄
    • 学会等名
      第21回ソフトウェア工学の基礎ワークショップ
    • 発表場所
      霧島国際ホテル、鹿児島県霧島市
    • 年月日
      2014-12-11 – 2014-12-13
    • 関連する報告書
      2014 実績報告書
  • [学会発表] Creating Confidence in the Correctness with formal methods and testing2014

    • 著者名/発表者名
      Toshiaki Aoki
    • 学会等名
      Integration of Formal Method and Testing for Model-Based Systems Engineering, Shonan Meeting
    • 発表場所
      Shonan Villlage Center, Hayama, Kanagawa
    • 年月日
      2014-12-01 – 2014-12-03
    • 関連する報告書
      2014 実績報告書
    • 招待講演
  • [学会発表] Sufficient completeness of parameterized specifications in CafeOBJ2014

    • 著者名/発表者名
      Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi
    • 学会等名
      12th Asian Symposium on Programming Languages and Systems, APLAS 2014
    • 発表場所
      Singapore, the Republic of Singapore
    • 年月日
      2014-11-17 – 2014-11-19
    • 関連する報告書
      2014 実績報告書
  • [学会発表] Generate & Check Method for Verifying Transition Systems in CafeOBJ (an overview)2014

    • 著者名/発表者名
      Kokichi Futatsugi
    • 学会等名
      Science and Practice of Engineering Trustworthy Cyber-Physical Systems, Shonan Meeting
    • 発表場所
      Shonan Villlage Center, Hayama, Kanagawa
    • 年月日
      2014-10-26 – 2014-10-30
    • 関連する報告書
      2014 実績報告書
    • 招待講演
  • [学会発表] Practical Application of Formal Methods to Automotive Systems2014

    • 著者名/発表者名
      Toshiaki Aoki
    • 学会等名
      Science and Practice of Engineering Trustworthy Cyber-Physical Systems, Shonan Meeting
    • 発表場所
      Shonan Villlage Center, Hayama, Kanagawa
    • 年月日
      2014-10-26 – 2014-10-30
    • 関連する報告書
      2014 実績報告書
    • 招待講演
  • [学会発表] モデル検査器により出力された反例に基づく誤り特定に関する研究2012

    • 著者名/発表者名
      陳適, 青木利晃
    • 学会等名
      情報処理学会 第177回ソフトウェア工学研究会
    • 発表場所
      大阪
    • 関連する報告書
      2012 実績報告書
  • [学会発表] 形式手法の研究と実践からざっくばらんに~産業界での可能性や今後の展望~2011

    • 著者名/発表者名
      青木利晃
    • 学会等名
      フォーマルメソッド普及促進セミナー2011 in札幌
    • 発表場所
      札幌(招待講演)
    • 年月日
      2011-07-22
    • 関連する報告書
      2011 実績報告書
  • [図書] Specification, Algebra, and Software: Essays Dedicated to Kokichi Futatsugi, LNCS 83732014

    • 著者名/発表者名
      Shusaku Iida, Jose Meseguer, Kazuhiro Ogata (Eds)
    • 総ページ数
      657
    • 出版者
      Springer
    • 関連する報告書
      2014 実績報告書
  • [図書] 組込みソフトウェア開発技術、9章組込みソフトウェアの静的検証技術(pp.271-307)2011

    • 著者名/発表者名
      青木利晃
    • 出版者
      CQ出版
    • 関連する報告書
      2011 実績報告書
  • [備考] CafeOBJ - Algebraic Specification and Verification

    • URL

      https://cafeobj.org

    • 関連する報告書
      2015 実績報告書
  • [備考] CafeOBJ: Algebraic Specification and Verification

    • URL

      http://cafeobj.org

    • 関連する報告書
      2014 実績報告書
  • [備考] CafeOBJ Official Website

    • 関連する報告書
      2013 実績報告書
  • [備考] JAIST RCSV Website

    • 関連する報告書
      2013 実績報告書
  • [備考] CafeOBJ Official Site

    • URL

      http://www.ldl.jaist.ac.jp/cafeobj/

    • 関連する報告書
      2012 実績報告書
  • [備考] JAIST Research Center for Software Verification

    • URL

      http://www.jaist.ac.jp/rcsv/index_e.html

    • 関連する報告書
      2012 実績報告書
  • [備考]

    • URL

      http://www.ldl.jaist.ac.jp/cafeobj/

    • 関連する報告書
      2011 実績報告書
  • [学会・シンポジウム開催] JAIST Mathematical Logic and Software Verification Joint Workshop2015

    • 発表場所
      Hotel Arrowle, Kaga-shi, Ishikawa, JAPAN
    • 年月日
      2015-12-03
    • 関連する報告書
      2015 実績報告書
  • [学会・シンポジウム開催] JAIST Software Verification Research Center Workshop2015

    • 発表場所
      Hotel Arrowle, Kaga-shi, Ishikawa, JAPAN
    • 年月日
      2015-06-25
    • 関連する報告書
      2015 実績報告書

URL: 

公開日: 2011-06-18   更新日: 2019-07-29  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi