Verification of Problem Models with Proof Scores

• Project/Area Number: 18300008
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: FUTATSUGI Kokichi Japan Advanced Institute of Science and Technology, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Kenkyū-buntansha): 中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (40345658)
• Co-Investigator(Renkei-kenkyūsha): NAKAMURA Masaki 金沢大学, 電子情報学系, 助教 (40345658)
• Project Period (FY): 2006 – 2009
• Project Status: Completed (Fiscal Year 2009)
• Budget Amount: ¥18,890,000 (Direct Cost: ¥15,200,000、Indirect Cost: ¥3,690,000); Fiscal Year 2009: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000); Fiscal Year 2008: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000); Fiscal Year 2007: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000); Fiscal Year 2006: ¥2,900,000 (Direct Cost: ¥2,900,000)
• Keywords: 仕様記述 / 仕様検証 / 形式手法 / 問題モデル / 証明スコア / 帰納法 / 場合分け / 仕様記述・仕様検証 / システム検証 / ソフトウェア工学 / 振舞仕様 / 安全性・信頼性 / 安全性 / 信頼性

Research Abstract

「帰納法」と「場合分け」は、問題モデル(問題領域や応用領域におけるモデル)の証明スコアによる検証法の基本技術である。本研究では、多様な応用分野で有効な帰納法と場合分けについて以下の成果を得た。(1)帰納法をデータ型・プロセス型の帰納的な構造に基づき定式化した。(2)場合分けを構成子からの項の生成に基づき定式化した。(3)(1),(2)に基づき、汎用的な証明規則を定式化するとともに、推論と探索を融合した強力な検証法を開発した。

Research Products

• [Journal Article] Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications (2010)
  • Author(s): Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: J. Symb. Comput 45(5) Pages: 551-573
  • NAID: 120003338960
  • Peer Reviewed
• [Journal Article] Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications (2010)
  • Author(s): 中村正樹, 緒方和博, Kokichi Futatsugi
  • Journal Title: J.Symb.Comput. 45(5) Pages: 551-573
  • NAID: 120003338960
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(1)-(6)、コンピュタソフトウェア (2009)
  • Author(s): 二木厚吉, 緒方和博, 中村正樹
  • Journal Title: 日本ソフトウェア科学会論文誌 25(2),25(2),25(3),25(4),26(1),26(2)
  • Peer Reviewed
• [Journal Article] Constructor-based institutions (2009)
  • Author(s): D. Gaina, K. Futatsugi, K. Ogata
  • Journal Title: Proc. of CALCO 2009 5728 Pages: 398-412
  • NAID: 110007110878
  • Peer Reviewed
• [Journal Article] User-Defined On-Demand Matching (2009)
  • Author(s): Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: IEICE Transactions 92-D(7) Pages: 1401-1411
  • NAID: 10026810203
  • Peer Reviewed
• [Journal Article] Constructor-based institutions (2009)
  • Author(s): Daniel Gaina, Kokichi Futatsugi, 緒方和博
  • Journal Title: Proc.of CALCO 2009, LNCS 5728, Springer Pages: 398-412
  • NAID: 110007110878
  • Peer Reviewed
• [Journal Article] User-Defined On-Demand Matching (2009)
  • Author(s): 中村正樹, 緒方和博, Kokichi Futatsugi
  • Journal Title: IEICE Transactions 92-D(7) Pages: 1401-1411
  • NAID: 10026810203
  • Peer Reviewed
• [Journal Article] Analysis of membership sharing problem in digital subscription services (2009)
  • Author(s): Jianwen Xiang, Jing Tian, 緒方和博, Kokichi Futatsugi, Akira Mori
  • Journal Title: International Journal of Revenue Management, Inderscience Enterprises Ltd. 13(3) Pages: 284-306
  • Peer Reviewed
• [Journal Article] CafeOBJ入門 (6)-通信プロトコルの検証 (2009)
  • Author(s): 緒方和博, 二木厚吉, 中村正樹
  • Journal Title: Iコンピュータソフトウェア (日本ソフトウェア科学会論文誌) 26(2) Pages: 284-306
  • NAID: 10025982447
  • Peer Reviewed
• [Journal Article] フォーマルメソッドの新展開-検証進化可能電子社会の中核技術- (2008)
  • Author(s): 二木厚吉
  • Journal Title: 情報処理 Vol.49,No.5 Pages: 521-529
  • Peer Reviewed
• [Journal Article] Checking Assignments of Controls to Risks for Internal Control (2008)
  • Author(s): Yasuhito Arimoto, Yuji Watanabe, Michiharu Kudoh, Kokichi Futatsugi
  • Journal Title: Proc. of 2nd International Conference on Theory and Practice of Electronic Governance 2008, ACM Pages: 98-104
  • Peer Reviewed
• [Journal Article] Verifying Design with Proof Scores (2008)
  • Author(s): K. Futatsugi, J.A. Goguen, K. Ogata
  • Journal Title: Proc. of 1st VSTTE, LNCS 4171, Springer Pages: 277-290
  • Peer Reviewed
• [Journal Article] A Specification Translation from Behavioral Specifications to Rewrite Specifications (2008)
  • Author(s): Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: IEICE Transactions 91-D(5) Pages: 1492-1503
  • NAID: 10026803820
  • Peer Reviewed
• [Journal Article] Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes (2008)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Proc. of the 10th Intl. Conference on Formal Engineering Methods (10th ICFEM) 5256 Pages: 187-206
  • Peer Reviewed
• [Journal Article] Formal digital license language with OTS/CafeOBJ method (2008)
  • Author(s): Jianwen Xiang, Dines Bjorner, Kokichi Futatsugi
  • Journal Title: Proc. of IEEE/ACS Intl. Conference on Computer Systems and Applications Pages: 652-660
  • Peer Reviewed
• [Journal Article] Simulation-based verification for invariant properties in the OTS/CafeOBJ method (2008)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Refine 2007, ENTCS 201, Elsevier Pages: 127-154
  • Peer Reviewed
• [Journal Article] CafeOBJ 入門(1)-形式手法とCafeOBJ, コンピュータソフトウェア (2008)
  • Author(s): 二木厚吉, 緒方和博, 中村正樹
  • Journal Title: 日本ソフトウェア科学会論文誌 25(2) Pages: 1-13
  • Peer Reviewed
• [Journal Article] Verifying Design with Proof Scores (2008)
  • Author(s): Kokichi Futatsugi, Joseph A. Goguen and Kazuhiro Ogata
  • Journal Title: 1st VSTTE, LNCS 4171, Springer Pages: 277-290
  • Peer Reviewed
• [Journal Article] 電子社会と法令工学 (2008)
  • Author(s): 片山卓也, 島津明, 東条敏, 二木厚吉, 落水浩一郎
  • Journal Title: 人工知能学会誌 23-4 Pages: 529-536
  • Peer Reviewed
• [Journal Article] フォーマルメソッドの新展開--検証進化可能電子社会の中核技術-- (2008)
  • Author(s): 二木厚吉
  • Journal Title: 情報処理(情報処理学会学会誌) 49-5 Pages: 521-529
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(1)-形式手法とCafeOBJ (2008)
  • Author(s): 二木厚吉, 緒方和博, 中村正樹
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-2 Pages: 1-13
  • NAID: 130004549105
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(2)-構文と意味 (2008)
  • Author(s): 中村正樹, 二木厚吉, 緒方和博
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-2 Pages: 14-27
  • NAID: 110006664763
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(3)-等式推論と項書換システム (2008)
  • Author(s): 中村正樹, 二木厚吉, 緒方和博
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-3 Pages: 69-80
  • NAID: 110006840405
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(4)-証明譜による検証法 (2008)
  • Author(s): 二木厚吉, 緒方和博, 中村正樹
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-4 Pages: 68-84
  • NAID: 130004549122
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(5)-認証プロトコルの検証 (2008)
  • Author(s): 緒方和博, 二木厚吉, 中村正樹
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 26-1 Pages: 71-83
  • NAID: 130004549136
  • Peer Reviewed
• [Journal Article] Maude : 書換え論理に基づく計算機言語および処理系 (2008)
  • Author(s): 緒方和博, 中村正樹, 二木厚吉
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-2 Pages: 78-84
  • NAID: 130004549110
  • Peer Reviewed
• [Journal Article] Verifying Design with Proof Scores (2008)
  • Author(s): Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata
  • Journal Title: Proc. of 1st VSTTE, Springer LNCS 4171 Pages: 277-290
  • Peer Reviewed
• [Journal Article] Formal digital licence language with OTS/CafeOBJ method (2008)
  • Author(s): Jianwen Xiang, Dines Bjorner, Kokichi Futatsugi
  • Journal Title: Proc. of IEEE/ACS Intl. Conference on Computer Systems and Applications Pages: 652-660
  • Peer Reviewed
• [Journal Article] Trace Anonymity in the OTS/CafeOBJ Method (2008)
  • Author(s): Weiqiang Kong, Kazuhiro Ogata, Jian Chen, Kokichi Futatsugi
  • Journal Title: Proceedings of the 8^<th>, International Conference on Computer and Information Technology (8^<th> CIT), IEEE Computer Society Press Pages: 754-759
  • NAID: 120006674345
  • Peer Reviewed
• [Journal Article] Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes (2008)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Proceedings of the 10th International Conference on Formal Engineering Methods (10th ICFEM), Springer LNCS 5256 Pages: 187-206
  • Peer Reviewed
• [Journal Article] Checking Assignments of Controls to Risks for Internal Control (2008)
  • Author(s): Yasuhito Arimoto, Yuji Watanabe, Michi haru Kudoh, Kokichi Futatsugi
  • Journal Title: Proc. of 2nd International Conference on Theory and Practice of Electronic Governance (2008), ACM Press Pages: 98-104
  • Peer Reviewed
• [Journal Article] Simulation-based verification for invariant properties in the OTS/CafeOBJ method (2008)
  • Author(s): Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: Proceedings of the 4th International Refinement Workshop(R, efine 2007), ENTCS201, Elsevier Pages: 127-154
  • Peer Reviewed
• [Journal Article] Specification and Verification of Workflows with RBAC Mechanism and SoD Constraints (2007)
  • Author(s): W. Kong, K. Ogata, K. Futatsugi
  • Journal Title: Intl. J. of Software Eng. and Knowledge Eng 17(1) Pages: 3-32
  • Peer Reviewed
• [Journal Article] On equality predicates in algebraic specification languages (2007)
  • Author(s): Masaki Nakamura, Kokichi Futatsugi
  • Journal Title: Proc. of the 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007) 4711 Pages: 381-395
  • Peer Reviewed
• [Journal Article] Modeling and verification of real-time systems based on equations (2007)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Sci. of Comp. Prog 66(2) Pages: 162-180
  • Peer Reviewed
• [Journal Article] Creme : An Automatic Invariant Prover of Behavioral Specifications, International Journal of Software Engineering and Knowledge Engineering (2007)
  • Author(s): Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura and Kokichi Futatsugi
  • Journal Title: World Scientific Vol.17, No.6 Pages: 783-804
  • Peer Reviewed
• [Journal Article] Modeling and verification of real-time systems based on equations, Science of Computer Programming (2007)
  • Author(s): Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: Elsevier 66(2) Pages: 162-180
  • Peer Reviewed
• [Journal Article] Specification and Verification of Workflows with RBAC Mechanism and SoD Constraints (2007)
  • Author(s): Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: International Journal of Software Engineering and Knowledge Engineering 17(1) Pages: 3-32
  • Peer Reviewed
• [Journal Article] Creme: An Automatic Invariant Prover of Behavioral Specifications (2007)
  • Author(s): Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura and Kokichi Futatsugi
  • Journal Title: International Journal of Software Engineering And Knowledge Engineering 17(6) Pages: 783-804
  • Peer Reviewed
• [Journal Article] Modehng and verification of real-time systems based on equations (2007)
  • Author(s): Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: Science of Computer Programming 66(2) Pages: 162-180
  • Peer Reviewed
• [Journal Article] Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm (2007)
  • Author(s): Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: IEICE TRANSACTIONS on Fundamental of Electronics, Communications and Computer Science E90-A(8) Pages: 1690-1703
  • NAID: 110007540867
  • Peer Reviewed
• [Journal Article] State Machines as Inductive Types (2007)
  • Author(s): Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: IEICE TRANSACTIONS on Fundamental of Electronics, Communications and Computer Science E90-A(12) Pages: 2985-2988
  • Peer Reviewed
• [Journal Article] Formalization and Analysis of Public Administration Domain with The OTS/CafeOBJ Method (2007)
  • Author(s): Xiaoyi Chen, Jianwen Xiang, Weigiang Kong and Kokichi Futatsugi
  • Journal Title: Proceedings of 3th International Conference on e-Government(ICEG 2007), ISBN1-905305-59-1ACL Pages: 77-86
  • Peer Reviewed
• [Journal Article] A License Language Design and Analysis for E.Govenment (2007)
  • Author(s): Xiaoyi Chen, Jianwen Xiang, Dines Bjorner and Kokichi Futatsugi
  • Journal Title: Proceedings of International Conference on Wireless Communications, Networking and Mobile Computing(WiCom 2007), ISBN1-4244-1312-5, IEEE Pages: 3445-3448
  • Peer Reviewed
• [Journal Article] Formal support for e-government system design with transparency consideration (2007)
  • Author(s): Xiaoyi Chen, Weiqiang Kong and Kokichi Futatsugi
  • Journal Title: Proceedimgs of the lstInternational Conference on Theory and Practice of Electronic Governance (ICEGOV 2007), ACM Pages: 20-29
  • Peer Reviewed
• [Journal Article] Algebraic Approaches to Formal Analysis of the Mondex Electronic Puxse System (2007)
  • Author(s): Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: Proceedings of the 6th International Conference on Integrated Formal Methods(6th IFM), LNCS4591, Speringer Pages: 393-412
  • Peer Reviewed
• [Journal Article] On equahty predicates in algebraic specification languages (2007)
  • Author(s): Masaki Nakamura and Kokichi Futatsugi
  • Journal Title: Proceedings of the 4th International Colloquium on Theoretical Aspects of Computing (ICTAC2007), LNCS4711, Springer Pages: 381-395
  • Peer Reviewed
• [Journal Article] 法令対象ドメインの形式記述と検証 (2007)
  • Author(s): 二木 厚吉, 緒方 和博, 有本 泰仁
  • Journal Title: 「法令工学の提案」, JAIST Press Pages: 71-93
• [Journal Article] Specification and Verification of Workflows with RBAC Mechanism and SoD Constraints (2007)
  • Author(s): Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: International Journal of Software Engineering and Knowledge Engineering 17・1 Pages: 1-30
• [Journal Article] Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method (2007)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Springer LNCS 4060 Pages: 596-615
  • NAID: 120000861107
• [Journal Article] モジュラーな代数仕様言語のための項書き換えシステム (2006)
  • Author(s): 中村正樹, 二木厚吉
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会論文誌) 23・3 Pages: 35-50
  • NAID: 110004815103
• [Journal Article] Verifying Specifications with Proof Scores in CafeOBJ (an invited keynote paper) (2006)
  • Author(s): Kokichi FUTATSUGI
  • Journal Title: Proc. of 21st IEEE International Conference on Automated Software Engineering Pages: 3-10
• [Journal Article] A Behavioral Specification of Imperative Programming Languages (2006)
  • Author(s): Masaki Nakamura, Watanabe, M., Kokichi Futatsugi
  • Journal Title: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences(電子情報通信学会論文誌) E89-A・6 Pages: 1558-1565
  • NAID: 110007502878
• [Journal Article] Automating Invariant Verification of Behavioral Specifications (2006)
  • Author(s): Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
  • Journal Title: Proceedings of the 6th International Conference on Quality Software (6^<th> QSIC) Pages: 49-56
• [Journal Article] Falsification of OTSs by Searches of Bounded Reachable State Spaces (2006)
  • Author(s): Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
  • Journal Title: Proceedings of the 18^<th> International Conference on Software Engineering and Knowledge Engineering (18th SEKE) Pages: 440-445
• [Journal Article] Induction-Guided Falsification (2006)
  • Author(s): Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
  • Journal Title: Springer LNCS 4260 Pages: 114-131
  • NAID: 120000861068
• [Journal Article] From Fault Tree Analysis to Formal Specification and Verification with OTS/CafeOBJ (2006)
  • Author(s): Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
  • Journal Title: Computer Software(コンピュータソフトウェア(日本ソフトウェア科学会論文誌)) 23・3 Pages: 134-146
• [Presentation] 実行可能な代数仕様の停止性証明について (2007)
  • Author(s): 中村 正樹, 二木 厚吉
  • Organizer: 情報科学技術レターズ(FIT2007)
  • Place of Presentation: 愛知県豊田市
  • Year and Date: 2007-09-21
• [Presentation] ドメインの形式記述と検証 (2007)
  • Author(s): 有本 泰仁, 二木 厚吉
  • Organizer: 電子情報通信学会研究報告
  • Place of Presentation: 石川県能美市
  • Year and Date: 2007-06-08
• [Presentation] Verifying Specifications with Proof Scores in CafeOBJ (2006)
  • Author(s): Kokichi FUTATSUGI
  • Organizer: Proc. of 21st IEEE International Conference on Automated Software Engineering
  • Place of Presentation: Tokyo
  • Year and Date: 2006-02-20
• [Presentation] Verifying Specifications with Proof Scores in CafeOBJ (invited keynote paper at ASE 2006, 20 September 2006, Tokyo) (2006)
  • Author(s): Kokichi Futatsugi
  • Organizer: Proc. Of 21st International Conference on Automated Software Engineering
  • Place of Presentation: IEEE
• [Book] 法令工学の提案(片山卓也) (2007)
  • Author(s): 二木厚吉,緒方和博,有本泰仁
  • Publisher: JAIST
• [Remarks] 以下のウェッブページを通じて、開発したシステムと例題、発表論文などを公開している。
  • URL: http://www.ldl.jaist.ac.jp/cafeobj
• [Remarks]
  • URL: http://www.ldl.jaist.ac.jp/cafeobj/
• [Remarks] 以下のウェッブページを通じて、開発したシステムと例題、発表論文などを公開している。
  • URL: http://www.ldl.jaist.ac.jp/cafeobj
• [Remarks]
  • URL: http://www.ldl.jaist.ac.jp/cafeobj