| 研究課題/領域番号 |
16K00010
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 埼玉大学 |
|---|
研究代表者 |
吉浦 紀晃 埼玉大学, 理工学研究科, 教授 (00302969)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2020-03-31
|
| 研究課題ステータス |
完了 (2019年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2018年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2017年度: 2,990千円 (直接経費: 2,300千円、間接経費: 690千円)
2016年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 時間論理 / プログラム合成 / モデル検査 / OpenFlow / リアクティブシステム / Safety Property / Liveness Property / Coq / 数理論理学 |
|---|
| 研究成果の概要 |
本研究の成果は、時間論理式の構文的な特徴からプログラム化可能性の性質の一種である強充足可能性や段階的充足可能性の判定が可能となるかを検討し、論理式の構造によりこれら２つの性質が一致することがあることを示した。また、これらの性質を効率よく判定することができることを明らかにした。しかし、構造が限定的であった。そこで、ネットワーク機器のソフトウェア、ロボット、自動車制御のネットワークシステムなどの検証すべき性質を記述してその構造を分析した。その結果、論理式の構造よりも、システムの動作を表す原子命題と利用者やシステムの外界の動作を表す原子命題の論理式の中の位置が重要であることを明らかにした。
|
| 研究成果の学術的意義や社会的意義 |
本研究の成果は、時間論理で記述されたリアクティブシステムの仕様の実現可能性の性質である強充足可能性と段階的充足可能性が、論理式の構造に特徴や制限がある場合に、同一になり、また、これらの性質が効率よく判定可能であることがわかった。このことは、プログラムの自動合成にとり重要な性質であり、安全なソフトウェアやシステムの開発に有効である。自動合成はバグのないソフトウェアの開発に重要であり、人手による開発によるバグの混入を防ぐことができる。
|
