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

2012 年度 研究成果報告書

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

研究概要

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

研究成果

• [雑誌論文] 要求・仕様参照モデルに基づく要求追跡の形式手法 (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 ページ: 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年度年会
  • 発表場所: 京都大学
  • 年月日: 20130300
• [学会発表] 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
  • 年月日: 20121200
• [学会発表] 命題時相論理の一階拡張について (2012)
  • 著者名/発表者名: 岡本圭史
  • 学会等名: 2010年日本数学会秋季総合分科会
  • 発表場所: 東京理科大学
  • 年月日: 2012-03-27
• [学会発表] 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
• [学会発表] Toward a Concise Proof ofCompleteness Theorem for PropositionalModal ￥mu-calculus (2010)
  • 著者名/発表者名: Yuki ANBO, Keishi OKAMOTO and AkitoTSUBOI
  • 学会等名: 2010年日本数学会秋季総合分科会
  • 発表場所: 名古屋大学
  • 年月日: 2010-09-22
• [学会発表] Jacksonの要求・仕様参照モデルに基づく要求追跡の形式手法 (2010)
  • 著者名/発表者名: 北村崇師,岡本圭史,武山誠
  • 学会等名: ソフトウェアエンジニアリングシンポジウム2010
  • 発表場所: 東洋大学
  • 年月日: 2010-09-01