2018 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 |
組込みシステムは、機能要件などの定性的制約に加えて、性能要件などの定量的制約を満たすことが強く求められる。定性的制約を満たすシステムの自動合成は国内外で研究されてきたが、定量的制約を同時に満たすシステム合成の研究は全く不十分であった。本研究では、形式手法を用いて、定性的制約に加えて、定量的制約として頻度制約と実時間制約を満たす、誤りがない組込みシステムを自動合成する手法を構成する。平成30年度は、頻度制約を満たすシステムの合成手法の研究」について、システム合成のおいては、状態遷移グラフを生成し、ゲームを構成する必要があるが、BDD(２分決定グラフ)を状態遷移グラフの遷移関係の表現のみに限定して部分的に用いることで、合成手続きを効率化した。さらに、ゲームを構成する際に、判定結果を変えない範囲でゲームを縮退させ単純化する手法を構成し、判定手続きを効率化した。「実時間制約を満たすシステムの合成手法」の研究について、LED点灯回路を例題とし、実時間制約を定性的に記述することを試みた。この結果、単純なメトリクスをもつ単純な形の実時間制約は、定性的に記述できた。
|
| 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
(5 results)
