2019 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 – 2021-03-31
|
| Keywords | 形式手法 / 定量的制約 / 組込みシステム / 自動合成 |
|---|
| Outline of Annual Research Achievements |
組込みシステムは、機能要件などの定性的制約に加えて、性能要件などの定量的制約を満たすことが強く求められる。定性的制約を満たすシステムの自動合成は国内外で研究されてきたが、定量的制約を同時に満たすシステム合成の研究は全く不十分であった。本研究では、形式手法を用いて、定性的制約に加えて、定量的制約として頻度制約と実時間制約を満たす、誤りがない組込みシステムを自動合成する手法を構成する。平成31年度は「頻度制約を満たすシステムの合成手法の研究」については、合成の効率化について取り組んだ。利得ゲームの質が高い戦略を得る際、最適戦略ではないがそれに近い解を効率的に得る手法の研究に取り組んだ。「実時間制約を満たすシステムの合成手法」について、前年度に引き続き、LED点灯回路を例題とし、実時間制約を定性的に記述することを試みた。実時間制約を定性的に記述する際に問題となるのは、割り込みなどによりプログラムの１ステップの時間幅が変化する場合である。この場合、定性的なプログラムの１ステップの実行に要する時間幅が変わってしまう。LEDの点灯回路においては、その変化をある程度見積もることが可能であった。この特徴を利用して、実時間制約を定性的に近似することに成功した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
「実時間制約を満たすシステムの合成手法の研究」について、定性的に記述可能な実時間制約を明らかにし、実時間制約から定性的制約への変換規則を与えているが、それを定式化するのに想定以上の時間を要していること。
|
| Strategy for Future Research Activity |
「頻度制約を満たすシステムの合成手法の研究」について、ひきつづき、合成の効率化について取り組む。利得ゲームの最適戦略に近い解を効率的に得る手法の研究に引き続き取り組む予定である。「実時間制約を満たすシステムの合成手法の研究についても、引き続き、定性的に記述可能な実時間制約を明確化し、さらに、実時間制約から定性的制約への変換規則を与える予定である。前年度行った、定性的に記述できない実時間制約を定性的制約での近似を、実時間制約から近似式への変換規則を与える予定である。そして、実時間制約に対する定性的記述と近似の正当性証明に取り組む予定である。
|
| Causes of Carryover |
以前から使用していた計算機が使用可能であり、これまでのところ、研究費で計算機を購入する必要がなかったこと、さらに、研究の遂行に予定より遅れ、予定していた研究発表を行わなかったことにより、次年度使用額が生じた。次年度は、計算機の購入及び研究発表のために、これを使用する計画である。
|
