論理式肥大に伴う活性のモデル検査の非効率化の改善

• 研究課題/領域番号: 23500041
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
• 研究期間 (年度): 2011 – 2013
• 研究課題ステータス: 完了 (2013年度)
• 配分額: 5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円); 2013年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円); 2012年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円); 2011年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: モデル検査 / 活性 / 公平性 / 準公平性 / 分割統治 / 公平性の理解 / 反例 / Maude / 状態機械

研究概要

公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。この論理式はBuchiオートマトンへ変換される。この変換は論理式の大きさに対しべき乗の計算と空間を必要とするため、公平性が大きくなるとBuchiオートマトンへの変換が実質不可能になり、モデル検査自体もできなくなる。本研究では、"公平性 ⇒ 準公平性"を満たし、公平性より小さな論理式である準公平性を探し、"準公平性 ⇒ 活性"をモデル検査することで公平性のもとでのモデル検査を可能とする方法を提案する。すなわち、"公平性 ⇒ 活性"の代わりに、"公平性 ⇒ 準公平性" と"準公平性 ⇒ 活性"をモデル検査することである。

研究成果

• [雑誌論文] A Divide & Conquer Approach to Model Checking of Liveness Properties (2013)
  • 著者名/発表者名: Kazuhiro Ogata and Min Zhang
  • 雑誌名: Proceedings of the 37th Annual International Computer Software & Applications Conference (37th COMPSAC), IEEE Computer Society Press ページ: 648-657
  • 査読あり
• [雑誌論文] Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions (2013)
  • 著者名/発表者名: Kazuhiro Ogata
  • 雑誌名: Proceedings of the 20th Asia-Pacific Software Engineering Conference (20th APSEC), IEEE ページ: 565-570
  • 査読あり
• [雑誌論文] Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions (2013)
  • 著者名/発表者名: Kazuhiro Ogata
  • 雑誌名: Proceedings of the 20th Asia-Pacific Software Engineering Conference 巻: 0 ページ: 565-570
  • DOI: 10.1109/apsec.2013.82
  • 査読あり
• [雑誌論文] A Divide & Conquer Approach to Model Checking of Liveness Properties (2013)
  • 著者名/発表者名: 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
  • 査読あり
• [雑誌論文] A Divide & Conquer Approach to Model Checking of Liveness Properties (2013)
  • 著者名/発表者名: Kazuhiro Ogata and Min Zhang
  • 雑誌名: Proceedings of the 37th Annual International Computer Software & Applications Conference (37th COMPSAC) 巻: 0 ページ: 0-0
  • 査読あり
• [雑誌論文] Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic (2012)
  • 著者名/発表者名: Kazuhiro Ogata and Phan Thi Thanh Huyen
  • 雑誌名: Proceedings of the 14th International Conference on Formal Engineering Methods (14th ICFEM) 巻: 7635 ページ: 87-102
  • 査読あり