ホーム

形式手法の産業応用ワークショップ

オーガナイサﾞ 実行委員長: 粂野文洋 (三菱総合研究所/国立情報学研究所)
実行委員:　來間啓伸(日立製作所/国立情報学研究所)
　　石川冬樹(国立情報学研究所)
　　田口研治(国立情報学研究所)
概要 ソフトウェアが社会の様々な製品やサービスに不可欠なものとなっている現在、ソフトウェアの不具合に起因するシステム障害は時として社会に広範囲かつ深刻な影響を与えています。こうした背景からソフトウェアの信頼性向上への要求がさらに求められつつあります。一方、海外においては、ソフトウェアを数学的基盤に基づいて論理的に検証しながら開発する形式手法についての研究開発が長年にわたり実施されており、実問題への適用が本格的に始まっています。日本においては、開発現場への普及が始まっているとはまだいえない状況にありますが、一部の開発現場においては適用が試みられ、人材育成の取り組みも始められています。
本ワークショップでは、国内において、形式手法の適用実践や人材育成を先駆的に取り組まれている有識者をゲストに迎え、各活動の現状や今後の構想について語っていただきます。また、形式手法の実践・教育に係る具体事例について、専門家にご紹介いただくとともに、形式手法の教育についてパネルディスカッションを開催し、企業における形式手法の教育の現状と課題について議論を致します。

予稿集 PDF版

プログラム

Session 1
(10:20-11:50)
形式手法の展望		 IPA/SECにおける形式手法に関する活動状況と課題
　山本修一郎　名古屋大学 情報連携統括本部 情報戦略室

予稿 PDF版

システム検証研究センターの七年間
　木下佳樹　産業技術総合研究所 システム検証研究センター

形式手法の知識体系 FMBoK (Formal Methods Body of Knowledge) 構築に向けて
　田口研治　国立情報学研究所　GRACE センター

Session 2
(14:20-15:50)
形式手法の実践・教育		 モデル検査知識体系 MCBOK2008 について
　西原秀明　産業技術総合研究所 組込みシステム技術連携研究体

ICカードセキュリティ開発における形式手法SPINの適用（Smartcard security development using formal method tool SPIN)
　市原尚久　（株）NTTデータ　技術開発本部 SIアーキテクチャ開発センタ

ソフトウェア開発における形式手法導入に関する課題と解決アプローチ
　石黒正揮　(株)三菱総合研究所　情報技術研究センター　情報セキュリティ研究グループ
Session 3
(16:10-17:40)
パネル　形式手法教育の現状と課題		 座長：粂野文洋　（株）三菱総合研究所／国立情報学研究所

企業内で形式手法教育を実践されている方々や研修セミナー・教育プログラム等で社会人を対象とした形式手法教育を実践されている方々をパネラとしてお招きし、各々の形式手法教育の現状についてご紹介いただくとともに、形式手法が開発現場に普及するための課題について人材育成の観点で議論していただきます。

パネリスト
　小川清　（名古屋市工業研究所）
　劉少英　（法政大学）
　青木利晃　（北陸先端科学技術大学院大学）
　来間啓伸　（日立製作所／国立情報学研究所）
　石川冬樹　（国立情報学研究所）