|
組込みシステムは、機能要件などの定性的制約に加えて、性能要件などの定量的制約を満たすことが強く求められる。定性的制約を満たすシステムの自動合成は国内外で研究されてきたが、定量的制約を同時に満たすシステム合成の研究は全く不十分であった。本研究では、形式手法を用いて、定性的制約に加えて、定量的制約として頻度制約と実時間制約を満たす、誤りがない組込みシステムを自動合成する手法を構成する。令和3年度は「頻度制約を満たすシステムの合成手法の研究」については、合成の効率化について引き続き取り組んだ。制約をモジュールに分割してシステムを合成できるが、どうモジュールにすれば合成が効率化されるのかは自明ではなかった。ここでは、モジュールの大きさと含まれる命題の種類の数を揃えることにより、効率化できることを明らかにした。「実時間制約を満たすシステムの合成手法」についても、引き続き、定性的に記述可能な実時間制約を明確化し、さらに、実時間制約から定性的制約への変換規則を与えるべく取り組んだ。定性的に記述できない実時間制約を定性的制約での近似として、その変換規則を与えるアプローチで取り組んだ。１単位時間を１ステップと捉えることを基本とするが、制御が他のプロセスに移っている場合などは１ステップをより長い時間と捉えることにより、実時間制約を定性的制約に置き換える規則を構成できた。
|
