2017 Fiscal Year Research-status Report
形式手法による定量的制約を満たす組み込みシステムの自動合成
| Project/Area Number |
16K00092
|
|---|
| Research Institution | Tohoku University of Community Service and Science |
|---|
Principal Investigator |
萩原 茂樹 東北公益文科大学, 公私立大学の部局等, 准教授 (70334547)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | 形式手法 / 定量的制約 / 組込みシステム / 自動合成 |
|---|
| Outline of Annual Research Achievements |
組込みシステムは、機能要件などの定性的制約に加えて、性能要件などの定量的制約を満たすことが強く求められる。定性的制約を満たすシステムの自動合成は国内外で研究されてきたが、定量的制約を同時に満たすシステム合成の研究は全く不十分であった。本研究では、形式手法を用いて、定性的制約に加えて、定量的制約として頻度制約と実時間制約を満たす、誤りがない組込みシステムを自動合成する手法を構成する。平成29年度は、「頻度制約を満たすシステムの合成手法の研究」について、合成の効率化に取り組んだ。仕様からシステム合成の一つの方法として、SATソルバを用いた有界システム合成手法があるが、その手法において、中間生成物であるオートマトンのシミュレーション関係を用いることにより、SAT問題を効率的に解き、システム合成を効率化する方法を考案した。さらに、システム合成可能性の近似とみなせる性質の一つとして強充足可能性があるが、その判定がシステム合成可能性よりも効率的に行えることを、現実的な仕様を例を用いて示した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
「頻度制約を満たすシステムの合成手法の研究」について、合成の効率化に寄与する複数のヒューリスティックを導入できたことによる。
|
| Strategy for Future Research Activity |
「頻度制約を満たすシステムの合成手法の研究」について、ひきつづき、合成の効率化について取り組む。我々が研究している無限長語オートマトンの縮約技術である、定性的制約の構文制限による手法を適用する予定である。また、利得ゲームの最適戦略に近い解を効率的に得る手法の研究にも引き続き取り組む予定である。また、システム合成手続きの正当性の証明に取り組む予定である。「実時間制約を満たすシステムの合成手法の研究について、第一に、定性的に記述可能な実時間制約を明確化し、実時間制約から定性的制約への変換規則を与える予定である。第二に、定性的に記述できない実時間制約を定性的制約での近似を試みる予定である。そして、実時間制約から近似式への変換規則を与える予定である。第三に、実時間制約に対する定性的記述と近似の正当性証明に取り組む予定である。
|
| Causes of Carryover |
（理由）
国際会議発表にかかる費用を、他の研究費で当てたため。
（使用計画）
国際会議発表、雑誌論文発表の費用に当てる予定である。今後、計算サーバを購入する必要がある場合、それを購入する予定である。
|
Research Products
(4 results)
