形式手法のための論理の構築と、一階拡張が満たす性質に関する研究

• 研究課題/領域番号: 22500021
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 仙台高等専門学校 (2011-2012); 独立行政法人産業技術総合研究所 (2010)
• 研究代表者: 岡本 圭史 仙台高等専門学校, 情報システム工学科, 准教授 (00308214)
• 研究分担者: 北村 崇師 産業技術総合研究所, セキュアシステム研究部門, 研究員 (70530484)
• 研究期間 (年度): 2011 – 2012
• 研究課題ステータス: 完了 (2012年度)
• 配分額: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2012年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2011年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2010年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
• キーワード: 数理論理学 / 形式手法 / 命題様相μ計算 / 一階様相μ計算 / モデル / 表現力 / 論理 / (論理の)表現力

研究概要

研究成果の概要(和文):対象を形式的に記述することで,それらの対象を自動的に検証できるようになる.しかし,形式的に記述・検証するためには,「論理」という枠組みが必要となる.本研究では,Jacksonモデルを基にした要求管理を目的とした論理やMilk-run物流システムの経路探索を目的とした論理を構築した.また,検証用論理として提案された一階様相μ計算に関する性質として,モデル論的性質や表現力比較に関するいくつかの性質をしめした

研究成果

• [雑誌論文] Automated route planning for milk-run transport logistics with the NuSMV model checker (2013)
  • 著者名/発表者名: Takashi Kitamura and Keishi Okamoto
  • 雑誌名: The IEICE Transactions on Information and Systems, Special Section on Parallel and Distributed Computing and Networking(Conditionally Accepted) 巻: ―
  • NAID: 130003385424
  • 査読あり
• [雑誌論文] 要求・仕様参照モデルに基づく要求追跡の形式手法 (2010)
  • 著者名/発表者名: 北村崇師,岡本圭史,武山誠, Jackson の
  • 雑誌名: Proceedings of the IPSJ/SIGSE ソフトウェアエンジニアリングシンポジウム ページ: 149-154
  • 査読あり
• [雑誌論文] Formal Verification ina First-Order Extension of Modal μ-calculus (2010)
  • 著者名/発表者名: Keishi Okamoto
  • 雑誌名: Information and MediaTechnologies 巻: 5(1) ページ: 40-47
  • 査読あり
• [雑誌論文] Comparing expressiveness of first-order modal μ-calculus and first-order CTL (2010)
  • 著者名/発表者名: Keishi Okamoto
  • 雑誌名: 京都大学数理解析研究所講究録 巻: 1708
• [雑誌論文] Formal Validation and Requirements Management Based on the Jackson's Reference Model for Requirements and Specifications (2010)
  • 著者名/発表者名: Takashi KITAMURA, Keishi OKAMOTO, Makoto TAKEYAMA
  • 雑誌名: Proceedings of the 16th IEEE Pacific Rim International Symposium on Dependable Computing 巻: (Published electronically)
  • 査読あり
• [雑誌論文] Jacksonの要求・仕様参照モデルに基づく要求追跡の形式手法 (2010)
  • 著者名/発表者名: 北村崇師, 岡本圭史, 武山誠
  • 雑誌名: Proceedings of the IPSJ/SIGSEソフトウェアエンジニアリングシンポジウム ページ: 149-154
  • 査読あり
• [雑誌論文] Formal Verification in a First-Order Extension of Modal μ-calculus (2010)
  • 著者名/発表者名: Keishi Okamoto
  • 雑誌名: Information and Media Technologies 巻: 5(1) ページ: 40-47
  • NAID: 130004549126
  • 査読あり
• [雑誌論文] Comparing expressiveness of first-order modal μ-calculus and first-order CTL* (2010)
  • 著者名/発表者名: Keishi Okamoto
  • 雑誌名: 京都大学数理解析研究所講究録 巻: 1708 ページ: 1-14
• [雑誌論文] Automated route planning for milk-runtransport logistics with the NuSMV modelchecker
  • 著者名/発表者名: Takashi Kitamura and Keishi Okamoto
  • 雑誌名: The IEICE Transactions onInformation and Systems, Special Sectionon Parallel and Distributed Computing andNetworking
  • 査読あり
• [雑誌論文] Formal Validation andRequirements Management Based on theJackson's Reference Model forRequirements and Specifications
  • 著者名/発表者名: Takashi KITAMURA,Keishi Okamoto,MakotoTAKEYAMA
  • 雑誌名: Proceedings of the 16th IEEE Pacific RimInternational Symposium on DependableComputing
  • 査読あり
• [学会発表] 一階時相論理の表現力について (2013)
  • 著者名/発表者名: 岡本圭史
  • 学会等名: 日本数学会2013年度年会
  • 発表場所: 京都大学
• [学会発表] 命題時相論理の一階拡張について (2012)
  • 著者名/発表者名: 岡本圭史
  • 学会等名: 2010年日本数学会秋季総合分科会
  • 発表場所: 東京理科大学
  • 年月日: 2012-03-27
• [学会発表] Anautomated route planning for milk-runtransport logistics using model checking (2012)
  • 著者名/発表者名: Takashi Kitamura, Keishi Okamoto
  • 学会等名: 4th International Workshop on Parallel andDistributed Algorithms and Applications
  • 発表場所: Okinawa, Japan
• [学会発表] An automated route planning for milk-run transport logistics using model checking (2012)
  • 著者名/発表者名: Takashi Kitamura, Keishi Okamoto
  • 学会等名: 4th International Workshop on Parallel and Distributed Algorithms and Applications
  • 発表場所: Okinawa, Japan
• [学会発表] 命題様相μ計算の一階拡張について (2012)
  • 著者名/発表者名: 岡本圭史
  • 学会等名: 仙台ロジックセミナー
  • 発表場所: 東北大学
• [学会発表] 検証のための論理構築 (2011)
  • 著者名/発表者名: 岡本圭史
  • 学会等名: 論理学的手法に基づくプログラム検証技術
  • 発表場所: 東北大学
  • 年月日: 2011-12-07
• [学会発表] Formal Validation and Requirements Management Based on theJackson's Reference Model forRequirements and Specifications (2010)
  • 著者名/発表者名: Takashi KITAMURA,Keishi Okamoto,MakotoTAKEYAMA
  • 学会等名: The 16thIEEE Pacific Rim International Symposiumon Dependable Computing
  • 発表場所: National Institute of Informatics,Tokyo, Japan
  • 年月日: 2010-12-15
• [学会発表] Formal Validation and Requirements Management Based on the Jackson's Reference Model for Requirements and Specifications (2010)
  • 著者名/発表者名: Takashi KITAMURA, Keishi OKAMOTO, Makoto TAKEYAMA
  • 学会等名: The 16th IEEE Pacific Rim International Symposium on Dependable Computing
  • 発表場所: National Institute of Informatics, Tokyo, Japan
  • 年月日: 2010-12-15
• [学会発表] Toward a Concise Proof ofCompleteness Theorem for PropositionalModal ￥mu-calculus (2010)
  • 著者名/発表者名: Yuki ANBO, Keishi OKAMOTO and AkitoTSUBOI
  • 学会等名: 2010年日本数学会秋季総合分科会
  • 発表場所: 名古屋大学
  • 年月日: 2010-09-22
• [学会発表] Toward a Concise Proof of Completeness Theorem for Propositional Modal \mu-calculus (2010)
  • 著者名/発表者名: Yuki ANBO, Keishi OKAMOTO, Akito TSUBOI
  • 学会等名: 2010年日本数学会秋季総合分科会
  • 発表場所: 名古屋大学
  • 年月日: 2010-09-22
• [学会発表] Jacksonの要求・仕様参照モデルに基づく要求追跡の形式手法 (2010)
  • 著者名/発表者名: 北村崇師,岡本圭史,武山誠
  • 学会等名: ソフトウェアエンジニアリングシンポジウム2010
  • 発表場所: 東洋大学
  • 年月日: 2010-09-01