| 研究課題/領域番号 |
26540026
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | プログラミング言語 / 実時間処理 / コード証明 / 分離論理 |
|---|
| 研究実績の概要 |
本年度は、プログラミング言語のモデルとなる時間に依存する計算モデルを研究するとともに、実時間オペレーティングシステムのコード証明を分離論理によって証明することを試みた。計算モデルについては、低レベルコードの振る舞いをモデル化する時間に依存した変数を持つ計算モデルとしてプロセス計算を拡張した計算体系を提案した。
プロセス計算モデルによって定式化することで、コンポーネントで構成されるソフトウェアを実現されているコードに基づいて検証するためのモデルを構成する手法の基礎についての研究を行った。
コード証明の手法の開発として実時間プログラムのオープンソースとして公開されているToppers OSを対象にして、タイミングに依存した振舞いが正確に実行されることを示す証明を構成することを試みた。マルチコア向けToppersOSにおいて、コア間でタスクをマイグレートするコードに対して証明を与えた。コードはC言語およびアセンブリ言語で記述されており、これらのコードに対して直接ルールを適用することによって正確にタスクがマイグレートされるかどうかについて証明を行った。ポインタによる意味を正確に表現する分離論理に対してビット操作など低レベルコードに適した表現を導入して証明を構成した。ここで、システムコールを実現する関数の意味とタスクマイグレーションの論理的意味づけにずれがあり、当初予想した性質の証明が構成できないことがわかった。コードの作成者への聞き取りによってこの性質については実際のコードとしてはバグではないことが判明したが、用いられる文脈から保証される概念であり、コード証明の有用性を向上させる上での問題点として挙げられる。作成した証明については機械的なチェックを行った後、２８年度に発表する計画である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
低レベルコードの証明手法については基本的な手順が確立できた。従来の低レベルコードの証明は、証明に適したプログラムコードに対して適用されているが、本研究は証明を意図しないオープンソースのプログラムコードへの適用を試みている。このため、構成される証明は対象のプログラミングスタイルに影響を受ける。また、オペレーティングシステムのシステムコールおいて、設計者の意図がコードに対応付けられているとは限らない。実用コードの証明における注意点がこれまでに判明した。
対象とした組み込み向け実時間オペレーティングシステムは、実用的には長期間利用されているため信頼性が高く、メンテナンスも実用に基づいて密に行われている。このため、今後、他のシステムコールについても証明が構成できる見通しを立てることができた。
これに対して、実時間性に関する証明に対する見通しは限定的である。この観点では、プロセス計算への変換を通じて証明を構成する手法のための、プロセス計算体系の拡張を今後も進める。
|
| 今後の研究の推進方策 |
従来の低レベルコードの証明体系が証明構成を意図したものであるため、その機械的証明体系も実際のコードとはギャップがあることがわかっている。今年度は、このギャップを埋めて構成したコード証明に対する定理証明器の適用に重点をおいて研究を進める。また、プログラムの再帰構造を表現できる時間依存のプロセス計算の体系における到達可能解析を進め、低レベルコードの実時間性を検証する体系についての見通しを得ることを目標とする。
|
| 次年度使用額が生じた理由 |
本研究にける結果発表が予定よりも遅れているため、旅費等の使用が見込みよりも少なかった。機械的定理証明についての調査から既存の証明体系がそのままでは利用できなかったため、そのための計算資源の用意ができなかったため、有効に活用するために計算機の購入を見送った。
|
| 次年度使用額の使用計画 |
２８年度は、機械的な証明手法（分離論理、時間プロセス計算）に重点を置いて研究を進める計画である。このための計算資源、ソフトウェアなどを調達して、本手法の実用性を示すために予算を使用する計画である。また、研究発表をより積極的に行って結果の提示に努める。
|
