2016 Fiscal Year Research-status Report
形式手法による定量的制約を満たす組み込みシステムの自動合成
| Project/Area Number |
16K00092
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
萩原 茂樹 東京工業大学, 情報理工学院, 助教 (70334547)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | 形式手法 / 定量的制約 / 組込みシステム / 自動合成 |
|---|
| Outline of Annual Research Achievements |
組込みシステムは、機能要件などの定性的制約に加えて、性能要件などの定量的制約を満たすことが強く求められる。定性的制約を満たすシステムの自動合成は国内外で研究されてきたが、定量的制約を同時に満たすシステム合成の研究は全く不十分であった。本研究では、形式手法を用いて、定性的制約に加えて、定量的制約として頻度制約と実時間制約を満たす、誤りがない組込みシステムを自動合成する手法を構成する。
平成28年度は「頻度制約を満たすシステムの合成手法の研究」について、頻度制約を満たすシステムを合成する機能のプロトタイプ実装に取り組んだ。具体的には、我々が既に構成した定性的制約を満たすシステム合成ツールに対して、頻度制約を満たすシステムを合成する機能、即ち、定性的制約から得た無限長語オートマトンを、頻度制約を用いて利得ゲームに変換し、利得ゲームの勝利戦略を導出する機能の実装に取り組んだ。利得ゲームの最適解を得るために、収束解を求めるアルゴリズムを用いている。このアルゴリズムでは、理論的に収束することを確認できるまでには大きな時間的コストがかかるが、ここでは、おおよそ収束した時点で、制約を満たすことを確認するヒューリスティックを導入した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(1)当初の目標の自動合成手法のプロトタイプ実装ができたこと、(2)効率化のためのヒューリスティック導入ができたことによる。
|
| Strategy for Future Research Activity |
「頻度制約を満たすシステムの合成手法の研究」について、合成の効率化について取り組む。我々が研究している2つの無限長語オートマトンの縮約技術（定性的制約の構文制限による手法、模倣関係を簡便に計算しオートマトンのサイズを小さくする手法）を適用する予定である。また、利得ゲームの最適戦略に近い解を効率的に得る手法の研究にも引き続き取り組む予定である。また、システム合成手続きの正当性の証明に取り組む予定である。
「実時間制約を満たすシステムの合成手法の研究について、第一に、定性的に記述可能な実時間制約を明確化し、実時間制約から定性的制約への変換規則を与える予定である。第二に、定性的に記述できない実時間制約を定性的制約での近似を試みる予定である。そして、実時間制約から近似式への変換規則を与える予定である。第三に、実時間制約に対する定性的記述と近似の正当性証明に取り組む予定である。
|
| Causes of Carryover |
東京工業大学情報理工学院西崎研究室のサーバを使用し、研究を推進することができ、購入予定だった計算サーバを購入しなかった。この費用を国際会議論文の作成、及び、国際会議発表にあてたが、わずかに剰余金がでた。
|
| Expenditure Plan for Carryover Budget |
今後、計算サーバを購入する必要がある場合、それを購入する予定である。購入する必要がない場合は、国際会議発表、雑誌論文発表の費用に当てる予定である。
|
