2012年研究カタログ
221/543

■ 研究担当:磯部祥尚/大岩寛/アフェルト レナルド/田中哲 ■ セキュアシステム研究部門 高信頼ソフトウェア研究グループ■ 連携担当:樋口哲也 高信頼ソフトウェア開発プロセス支援ツールの研究研究のポイント研究のねらい研究内容連携可能な技術・知財 ●ソフトウェア開発プロセスに支援ツールを導入し、人間の不注意による不具合を削減する ●数学に基づく厳密な形式手法・ツールを適用し、ソフトウェアの信頼性を向上させる ●手法・ツールの組合せを選択可能にし、信頼性と開発コストをバランスさせる 近年、様々な機械制御や情報処理にソフトウェアが使われており、年々その規模は増加し、その機能は多様化・複雑化しています。そのため、人間の不注意によって生じる不具合も増加し、潜在化した不具合がリリース後に発見されることもあります。本研究では、設計工程から実装工程にかけて形式手法を適用し、不具合の予防や早期発見を可能にする開発プロセスの確立、及び、その支援ツールの開発・普及を目指しています。また、信頼性と開発コストをバランスさせるため、形式手法と従来手法を併用する方法も研究しています。 設計工程において、複数のプロセスの協調動作を自動的に解析するツールCONPASUを研究開発しています(図1参照)。間違えやすい協調動作は厳密に解析し、逐次動作の解析には従来手法を併用できます。実装工程において、プログラムが仕様通りに実装されていることを定理証明器Coqで厳密に証明する方法を研究しています(図2参照)。証明の正当性を保証するだけでなく、再利用可能な定義や証明ライブラリを蓄積して、ユーザビリティの向上にも貢献しています。形式仕様から参照実装を生成するツールの開発や、それらツールの連携方法を研究しています。●CONPASU:並行プロセス動作解析ツール (産総研知財管理番号H24PRO-1409)● seplog:C言語及びアセンブリ言語による実装のCoqによる形式検証基盤 (産総研知財管理番号H22PRO-1175)● プロトコル仕様書からの参照実装・ブラックボックステストの自動生成ツール● 網羅テストの効率化・確実化のための仮想機械モニタ・連携ツール図1 CONPASUツールによる仕様の解析例図2 定理証明器Coqによる実装の証明例● 研究拠点つくば中央219情報通信・エレクトロニクス分野第2会場I-54I-54

元のページ 

page 221

※このページを正しく表示するにはFlashPlayer10.2以上が必要です