Realizability Decision and Program Synthesis for Reactive System Specification described by Temporal Logic
Project/Area Number |
25330008
|
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 |
YOSHIURA Noriaki 埼玉大学, 情報メディア基盤センター, 准教授 (00302969)
|
Project Period (FY) |
2013-04-01 – 2017-03-31
|
Project Status |
Completed (Fiscal Year 2016)
|
Budget Amount *help |
¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2015: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2014: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2013: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
Keywords | 時間論理 / モデルチェッキング / 実現可能性 / リアクティブシステム / 適切さの論理 / 仕様記述 / プログラム化可能性 / 仕様検証 |
Outline of Final Research Achievements |
The research proposed the decision method that determinizes the realizabilities of reactive system specifications that are described in temporal logic. The method consists of the inference rules and the automata and can determine the unrealizibilties of the specifications fast. The research proposed the method of deducing constraint formulas of requirement for unrealizable reactive system specifications. The contraint formulas are useful to revise unrealizable reactive system specifications so that they may be realizable. The research also improves the inference system of relevant logic. The inference rule can deduce information from reactive system specifications. The information is useful so that the descriptors of the specifications can verify that the specifications are equal to what the specifications should be. Moreover, the research proposed the verification method of OpenFlow software. The method can be a base of synthesizing OpenFlow software from network topologies.
|
Report
(5 results)
Research Products
(14 results)