| 研究課題/領域番号 |
24500051
|
|---|
| 研究機関 | 独立行政法人産業技術総合研究所 |
|---|
研究代表者 |
AFFELDT Reynald 独立行政法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
大岩 寛 独立行政法人産業技術総合研究所, 情報・人間工学領域研究戦略部, 主任研究員 (20415649)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2016-03-31
|
| キーワード | Coq / 定理証明支援系 / C言語 / アセンブリ言語 |
|---|
| 研究実績の概要 |
本研究は、組込み応用向けプログラムを検証するために、動作環境の差異と移植性を考慮したC言語のモデルとその論理を形式化することを目的にしている。平成２４年度にアセンブリ言語の形式検証基盤を整備し、平成２５年度にC言語の形式検証を整備した。同時に、平成２４年度以降、低レベルプログラミング言語に関する研究をサーベイし、関数呼出の形式検証基盤のプロトタイプを準備した。平成２６年度以降、移植性のあるC言語とプラットフォームに依存するアセンブリを混合するプログラムの形式検証基盤の整備を開始した。
平成２６年度にC言語の形式検証基盤に関する論文が国際学術雑誌に採択され、掲載された。上記の論文を改良し、C言語の形式検証基盤を向上した。その際、ツールとして用いている定理証明支援系の形式検証検査の効率（速度）が、予想外に低下していることが分かった。一方、平成２４年度に整備したアセンブリ言語の形式検証基盤との統合に向けて、上記のC言語の形式検証基盤の拡張を始めた。具体的には、関数呼び出しを定式化し、ローカル変数を導入し、健全性と完全性を形式化した。更に、グローバル変数を用いて拡張し、分離論理のフレームルールの形式化を開始した。最終的にC言語とアセンブリ言語を統合した形式検証基盤を構築する予定だったが、上記の効率の問題に加えて、研究の分担者の一時的な所内移動によって、必要な準備や議論が遅れた。そのため、平成２６年度に、計画を変更し、本研究の代表者は本研究の成果普及となる講演等の活動を増やした。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
本研究の目的は組み込み用のプログラムのための定理証明支援系の形式検証基盤の構築である。そのため、平成２４年度と平成２５年度に整備したアセンブリ言語とC言語の形式検証基盤を統合する計画を立てた。しかしこれは、定理証明支援系の形式検証検査の効率低下の問題によって予想より困難であった。更に、本研究の分担者の一時的な所内移動によって、統合に必要な議論と準備が遅れた。
|
| 今後の研究の推進方策 |
C言語の形式検証基盤を関数呼び出しで拡張し、C言語とアセンブリ言語を両方扱える基盤を構築・整理し、その結果に基づく研究発表を行い、論文を作成する。平成２６年度に生じたパフォーマンスの問題について、次年度に行われる定理証明支援系の開発者会議に参加し、定理証明支援系Coqの開発者と議論する。アセンブリ言語とC言語を混合するケーススタディーを選定するために、センサーネットワーク用のオペレーティングシステムのアプリの一例を検討し、組込みシステムのセキュリティに関する研究を行っている海外の専門家を訪問する。
|
| 次年度使用額が生じた理由 |
平成２６年度に、C言語の形式検証基盤を完成し、ケーススタディー実験及びアセンブリ言語と形式検証基盤の統合を行う予定であったが、研究分担者の一時的な異動等により研究の進歩に遅れが生じたため、未使用額が生じた。
|
| 次年度使用額の使用計画 |
このため、C言語とアセンブリ言語の双方を扱える基盤の構築・整理、アセンブリ言語とC言語を統合するケーススタディー例の選定と論文の作成・発表を次年度に行うこととし、未使用金額はその経費に当てることとしたい。
|
