2020 Fiscal Year Research-status Report
形式手法による定量的制約を満たす組み込みシステムの自動合成
| Project/Area Number |
16K00092
|
|---|
| Research Institution | Chitose Institute of Science and Technology |
|---|
Principal Investigator |
萩原 茂樹 公立千歳科学技術大学, 理工学部, 准教授 (70334547)
|
|---|
| Project Period (FY) |
2016-04-01 – 2022-03-31
|
| Keywords | 形式手法 / 定量的制約 / 組込みシステム / 自動合成 |
|---|
| Outline of Annual Research Achievements |
組込みシステムは、機能要件などの定性的制約に加えて、性能要件などの定量的制約を満たすことが強く求められる。定性的制約を満たすシステムの自動合成は国内外で研究されてきたが、定量的制約を同時に満たすシステム合成の研究は全く不十分であった。本研究では、形式手法を用いて、定性的制約に加えて、定量的制約として頻度制約と実時間制約を満たす、誤りがない組込みシステムを自動合成する手法を構成する。令和2年度は「頻度制約を満たすシステムの合成手法の研究」については、合成の効率化について引き続き取り組んだ。利得ゲームの最適戦略ではないがそれに近い解を効率的に得る手法の研究に取り組んだ。「実時間制約を満たすシステムの合成手法」についても、引き続き、定性的に記述可能な実時間制約を明確化し、さらに、実時間制約から定性的制約への変換規則を与えるべく取り組んだ。ここで、定性的に記述できない実時間制約を定性的制約での近似として、その変換規則を与えるアプローチで取り組んだ。一般に、近似式が大きくなるとシステム合成の障害となる。実時間制約の実時間の粒度を粗くすることで、近似式の大きさを抑えるアプローチを取っている。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
COVID-19のまん延により、研究に使える時間が限定的であったこと。さらに、「実時間制約を満たすシステムの合成手法の研究」について、定性的に記述可能な実時間制約を明らかにし、実時間制約から定性的制約への変換規則を与えているが、それを定式化するのに想定以上の時間を要していること。特に制約式の大きさが合成にかかるコストに大きく影響するが、そのための考察と対策に時間を要していること。
|
| Strategy for Future Research Activity |
「実時間制約を満たすシステムの合成手法の研究について、引き続き、定性的に記述可能な実時間制約を明確化し、さらに、実時間制約から定性的制約への変換規則を与える予定である。定性的に記述できない実時間制約を定性的制約での近似を、実時間制約から近似式への変換規則を与える予定である。このとき、近似式の大きさについても深く考察する予定である。そして、実時間制約に対する定性的記述と近似の正当性証明に取り組む予定である。
|
| Causes of Carryover |
COVID-19のまん延により、研究の遂行に予定より遅れ、予定していた研究発表を行わなかったこと、国際学会や国内学会が、COVID-19のまん延によりオンラインで行われ、旅費や宿泊費を計上する必要がなかったことにより、年度使用額が生じた。次年度はこの研究発表と必要な計算資源を整えるためにこれを使用する計画である。
|
