○国内プロジェクト
| プロジェクト | モデル検査による組込みソフトウェア検証とモデリング・パターン化の研究開発(新世代情報セキュリティ研究開発事業) |
| 実施者等 | 三菱総合研究所, 日立ソリューションズ、NII、早稲田大学、NTTデータ（経済産業省委託事業） |
| 概要 | 実システムに対してモデル検査等の形式手法の適用に関するケーススタディを実施するとともに、得られた知見や実応用事例に関する調査などをもとに、開発現場に形式手法を導入する上でのマネジメント面、技術面に関する方法や留意点をガイダンスにまとめ、普及啓発活動を行った。 |
| 実施期間 | 2008年度～2010年度(3ヵ年) |
| 連絡先 | 三菱総合研究所 情報技術研究センター 石黒正揮 TEL:03-6705-6047 |
| URL | http://formal.mri.co.jp/ |
| プロジェクト | 開放型分散環境でのソフトウェア部品検証システムの研究開発 |
| 実施者等 | JAIST, SRA, 三菱総合研究所, ユニシス（IPA事業） |
| 概要 | ソフトウェア部品とそれに対応した代数仕様記述言語を用いた形式手法からなるデータベースを構築し、ソフトウェアの性質やインタフェース等の仕様を条件として関連するソフトウェア部品を検索したり検証するシステムを開発した。 |
| 期間 | 1999～2001年度(3ヵ年） |
| 連絡先 | ― |
| URL | ― |
| プロジェクト | ネットワーク上で統合された代数仕様言語環境の研究開発 |
| 実施者等 | JAIST, 三菱総合研究所, SRA, ユニシス, NEC, 日立、管理工学研究所（IPA事業) |
| 概要 | WEBブラウザを用いてインターネット上でソフトウェアの代数仕様を作成、形式検証、管理を行うためのシステムを開発した。 |
| 期間 | 1996～1997年度(2ヵ年) |
| 連絡先 | ― |
| URL | ― |
| プロジェクト | 高信頼ソフトウェア構築技術に関する動向調査(2007 年度産学連携ソフトウェア工学実践拠点) |
| 実施者等 | 三菱総合研究所(経済産業省委託事業) |
| 概要 | 重要インフラ等システムの信頼性を保つ技術を確立することを目的とし、重要インフラ等を実現するためのシステム基準や形式手法の適用事例を調査・ヒアリングし、高信頼システム構築に向けての形式手法を分析・整理した。また、有識者による調査検討会、及びフォーラムを開催し、高信頼システムを実現するための課題や提言をまとめた。 |
| 期間 | 2007年度 |
| 連絡先 | 三菱総合研究所 情報技術研究センター |
| URL | http://sec.ipa.go.jp/reports/20080606.html |
| プロジェクト | セキュアプロトコルに対する攻撃法等に関する技術調査 |
| 実施者等 | 三菱総合研究所(IPA事業) |
| 概要 | セキュアプロトコルの攻撃法や形式手法を用いた検証等に関する技術動向調査を行った。 |
| 期間 | 2003年度 |
| 連絡先 | 三菱総合研究所 情報技術研究センター 石黒正揮 TEL:03-6705-6047 |
| URL | ― |
| プロジェクト | セキュリティプロトコルに対する既存攻撃手法及び安全性検証手法の調査 |
| 実施者等 | 三菱総合研究所（民間委託） |
| 概要 | セキュリティプロトコルに対する既存攻撃手法と安全性の検証手法に関する調査を行った。安全性の検証については、従来の計算論的安全性と形式手法に基づく記号論的安全性の両方を融合した新しい研究動向などの調査を行った。 |
| 期間 | 2006～2007年度 |
| 連絡先 | 三菱総合研究所 情報技術研究センター 石黒正揮 TEL:03-6705-6047 |
| URL | ― |
| プロジェクト | 組込みシステムの先端的モデルベース開発実態調査 |
| 実施者等 | 三菱総合研究所(IPA事業) |
| 概要 | 日本におけるモデルベース開発の実態を調査し、組込みシステム開発に於けるモデルベース開発（主に形式手法以外）を促進し、日本の組込みシステム産業の開発力強化に資するレポートをまとめた。 |
| 期間 | 2010年度 |
| 連絡先 | 三菱総合研究所 情報技術研究センター |
| URL | ― |
| プロジェクト | セキュアプログラミングのためのプログラム静的解析 |
| 実施者等 | 三菱総合研究所(JST委託事業） |
| 概要 | ソフトウェアのソースコードを静的解析することにより、バッファオーバーフローやメモリーリーク等のセキュリティ上の不具合（脆弱性）を検出するシステムを開発した。 |
| 期間 | 2003～2005年度 |
| 連絡先 | 三菱総合研究所 情報技術研究センター 石黒正揮 TEL:03-6705-6047 |
| URL | ― |
| プロジェクト | 形式手法適用調査 |
| 実施者等 | IPA |
| 概要 | 欧米における形式手法実応用プロジェクト、形式手法ツールベンダ、形式手法の技術者向け教育研修等を調査・分析し、また国際標準等における形式手法の適用例を整理した。 |
| 期間 | 2009年度 |
| 連絡先 | 情報処理推進機構(IPA) SEC |
| URL | http://sec.ipa.go.jp/reports/20100729.html |
| プロジェクト | トップSEプログラム（産業融合高度人材養成拠点の形成） |
| 実施者等 | NII, 協賛企業 |
| 概要 | 将来に向けて産業界と大学との技術的なギャップの解消を目指し、形式手法を含むソフトウェア工学に関する講座を提供している。 |
| 期間 | 2006年度から |
| 連絡先 | ― |
| URL | http://www.topse.jp/ |
| プロジェクト | 組込みシステム技術連携研究体 |
| 実施者等 | 産業技術総合研究所 組込みシステム技術連携研究体 |
| 概要 | システム検証の科学技術に関する研究情報を学界および産業界から広く集約し、さらに、産学官連携を推進し、この分野の研究開発と人材育成ることをミッションとした組織。 |
| 期間 | 2010年度から |
| 連絡先 | ― |
| URL | http://cfv.jp/cvs/ |
| プロジェクト | ソフトウェア独立検証と有効性確認(IV&V) |
| 実施者等 | JAXA 情報・計算工学センター |
| 概要 | 開発部門とは資金的、組織的に独立した部門が、独立した視点と技術によって、宇宙機ソフトウェアの課題や問題を洗い出し、潜在するリスクを軽減する活動を行っている。ソフトウェアが宇宙機のミッションを実現するための要件を満たしていること、また、設計やテストの内容が要求事項に適合していることを、文書レビュー、モデル検査、解析、シミュレーションなどの手法を用いて、様々な視点で評価する。 |
| 期間 | ― |
| 連絡先 | ― |
| URL | http://stage.tksc.jaxa.jp/jxithp/ |
○海外プロジェクト
| 海外 | DESTECS (Design Support and Tooling for Embedded Control Software)(Overture Projecet (VDM)（新規）) |
| 実施者 | Twente大学, Newcastle大学, Arhus工科大学等（EU FP7プロジェクト） |
| 概要 | フォルトトレラント組込みシステム開発に関わる課題解決に取り組むコンソーシアムである。欧州FP7の研究資金を得て、組込みリアルタイム制御システムのツールや方法論の開発を行う。形式手法のVDM++の開発プラットフォームの研究を行っている。 |
| 期間 | 2010年度～2013 |
| 連絡先 | ― |
| URL | http://www.destecs.org/summary.html |
| 海外 | DEPLY |
| 実施者 | Newcastle大学、シーメンスTS、SAP、ClearSyなど（EU FP7プロジェクト） |
| 概要 | 形式手法のEvent-Bに関するRODINプラットフォームの継続開発を行う。また、鉄道のCBTCシステム、自動車のクルーズコントロールシステム、宇宙分野等の適用事例研究を行う。 |
| 期間 | 2008/2～2013/1(5年間） |
| 連絡先 | ― |
| URL | http://www.deploy-project.eu/html/about_deploy_project.html |
| 海外 | Rodin Platform (Event-B) |
| 実施者 | Newcastle大学、Praxis HIS、ClearSyなど（EU FP6プロジェクト） |
| 概要 | 形式手法のEvent-B表記の開発、EclipseベースのRODINプラットフォームの開発を行う。また、航空管制ディスプレイ、エンジン障害管理等の適用事例研究を行う。 |
| 期間 | 2004～2007 |
| 連絡先 | ― |
| URL | http://www.event-b.org/ |
| 海外 | EASIS project(Electronic Architecture and System Engineering for Integrated Safety Systems） |
| 実施者 | Bosch, Daimler-Chryser, FIAT, MIRA, VALVOなど（EU FP6プロジェクト） |
| 概要 | 自動車分野の高安全なシステム開発技術の研究開発プロジェクトであり、その成果物として、モデル検査の適用に関する実践的で、有用なノウハウをまとめたガイドブックを作成している。ガイドブックは、自動車分野以外でも組込みシステム分野で参考になる。形式手法に関するプロジェクトマネジメントや費用対効果などについては殆ど書かれていない。 |
| 期間 | 2003年～2006年 |
| 連絡先 | ― |
| URL | http://ec.europa.eu/information_society/activities/esafety/doc/rtd_projects/fact_sheets_fp6/easis.pdf |
| 海外 | Grand Challenge in Dependable System Evolution (GC6) |
| 実施者 | York大学等(UK CRC, EPSRCプロジェクト） |
| 概要 | Verified Software Initiative(VSI)の活動により、数百のプログラムやモジュールについて仕様、設計、テストケース、修正履歴、形式文書、非形式文書を整備したVerified Software Repositoryを構築する。これにより高信頼性を確保するコンピュータシステム構築を可能にする。その中に含まれるVerified Compiler は、プログラムを実行する前に、その正しさを証明するツールである。VSIの活動には、TokeneerやMODEXなどの検証事例が含まれる。 |
| 期間 | 2004年開始。10～15年間 |
| 連絡先 | ― |
| URL | http://www.google.co.jp/url?sa=t&source=web&cd=1&ved=0CB4QFjAA&url=http%3A%2F%2Fqpq.csl.sri.com%2Fvsr%2Fprivate%2Fieee-computer-final.pdf&ei=eUHjTe-rEI6KvgPYh5GhAQ&usg=AFQjCNGelIRH9-ErnaQ8qYRe0gf7nS4fEw |
| 海外 | NASA Software Program |
| 実施者 | NASA |
| 概要 | 既存のシステム開発に形式手法を導入するための管理者、技術者向けの情報を提供するガイドブック"FORMAL METHODS SPECIFICATION AND VERIFICATION GUIDEBOOK FOR SOFTWARE AND COMPUTER SYSTEMS, VOLUME I: PLANNING AND TECHNOLOGY INSERTION, Volume II: A Practitioner's Companion"を作成した。NASA Safety and Mission ualit |
| 期間 | 1996年～1998年 |
| 連絡先 | ― |
| URL | http://eis.jpl.nasa.gov/quality/Formal_Methods/ |