| Project/Area Number |
16K00010
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Project Status |
Completed (Fiscal Year 2019)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 時間論理 / プログラム合成 / モデル検査 / OpenFlow / リアクティブシステム / Safety Property / Liveness Property / Coq / 数理論理学 |
|---|
| Outline of Final Research Achievements |
This research discusses whether the syntactic features of temporal logic formulas can be used for decision of strong satisfiability and stepwise satisfiability, which are properties of programability of program specification. The research finds that these two propoerties are the same under some restricted structure of formulas and that the restriction of logical formulas enables to determine the two properties effectively. The restriction, however, is too severe and the research investigates weak restriction of logical formulas for effective determination of the two properties.
The research describes several properties for practical systems or software such as software for network devices, robots, and network systems for automotive control to investigates the structure of formulas for practical systems. The investigation shows that the positions of atomic formulas which expresses behaviors of environment of the system are important for determination of the two properties.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究の成果は、時間論理で記述されたリアクティブシステムの仕様の実現可能性の性質である強充足可能性と段階的充足可能性が、論理式の構造に特徴や制限がある場合に、同一になり、また、これらの性質が効率よく判定可能であることがわかった。このことは、プログラムの自動合成にとり重要な性質であり、安全なソフトウェアやシステムの開発に有効である。自動合成はバグのないソフトウェアの開発に重要であり、人手による開発によるバグの混入を防ぐことができる。
|
