| 研究課題/領域番号 |
26540026
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | 実時間性検証 / 分離論理 / コード証明 / スーパーバイザ制御 / Nested Timed Automaton |
|---|
| 研究実績の概要 |
本研究では、実時間性が重要な性質である組込みシステムなどの実行基盤として用いられる実時間オペレーティングシステム(RTOS)上で構成される実時間システムが実時間性を含めて正しく振る舞うことを検証する手法を確立する。
平成２６年度は、ソフトウェアの実時間性モデルに関する研究と分離論理によるオペレーティング・システムの低レベルのコードの手動証明を実施した。前者については、申請者が従来研究を行っているNeTA(Nested Timed Automata)についての到達可能性についての近似アルゴリズムを提案した[LNCS8979]。後者については、オープンソースの組み込み向けRTOSであるToppers/SSPカーネルに対して分離論理を用いて証明を与えた。[信学技報 vol.114-510] SSPカーネルは少量のメモリで動作する実用的RTOSである。分離論理に対してビット操作の表現を導入することによって、Toppers/SSPカーネルのソースコード自体に証明を与えることが可能であることを示した。ここでは、インラインアセンブリ言語を含む例レベルなソースコードを対象とすることができた。
RTOSでは実時間性を確保するために割り込みが利用されるが、このための近似検証手法についても検討した。検証手法を実際のコード手法に適用していく手法について今後検討を行う。
関連して、実時間システムのシステム制御に対する検証手法に対する研究を進めた。主にスーパバイザ合成について、従来から提案されている方法に対して、SMTソルバによる新たな解法を検討した[信学技報 114-271,114-476]。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
コード証明について初歩的な結果を得ることができた。本研究の対象となるRTOSのToppers/SSPカーネルコードの一部に対して証明を与えた。ただし、証明に対するコストは予想どおりに大きく、特に適切なループインバリアントの導出に時間を要した。この点は、既存研究から予想された範囲であるが、その効率化手法については新たな研究が必要であることがわかった。証明を構成するにあたって、既存のコード証明に対する調査を行い、機械的証明の体系についても検討した。既存研究において、コード証明の手法と実現がいくつか提案されているがいずれも実験的であったり、目的に違いがあり、今後コード証明を効率的に進めるためには、RTOSコードに適した証明支援環境の構築が必要であることがわかった。ビット操作の表現を導入することによって、カーネルコード全体に証明を与えることが可能であるので、証明を支援する環境を今後整備する必要があることがわかった。
|
| 今後の研究の推進方策 |
今後は、まず証明支援環境の構築を定理証明支援系coq上に整備する。既存のコード証明支援系は、研究終了後から時間が経過しているためそのままでは、現在のcoq証明系では動作しない。また、ビット操作のためのライブラリを充実させることにより、証明の効率化を図る。
理論的なトピックとして、分離論理におけるループインバリアントの導出がある。線形方程式のテンプレートを用意して良好なループインバリアントを得る既存研究があるが、分離論理におけるループインバリアントへの適用を試みる。機械証明による効率化とともにコード証明の効率向上を目指す。
さらに実時間性については、微分動的論理式の記述を導入して証明体系に導入することを検討する。
|
| 次年度使用額が生じた理由 |
物品が当初計画よりも低額で同等の性能を満たすものが購入できたこと、また、出張費用のうち安価な航空料金が適用できたことによる。研究の進捗に応じた最適な物品購入および旅費支出としたことによる。
|
| 次年度使用額の使用計画 |
研究の進捗に応じて、機械的証明の必要性が知見として得られたため、証明が効率的に可能になる計算機を導入すること、また、できるだけ海外での学会に投稿して発表することで研究を進めていくことで当該予算を使用していく計画である。
|
