研究開発された技術紹介

我が国のものづくり産業では、組込みソフトウェア開発量の爆発的増加によりソフトウェアに起因する重大不具合が増加し、多大な社会損失を招いている。不具合の多くは仕様の曖昧性が原因であり、欧米諸国では形式手法の導入による対策に積極的に取り組んでいるが、国内での普及は進んでいない。本研究では実製品への形式手法適用技術の確立により上流の不具合流出率を半減させ、我が国組込みソフトウェアの高信頼性確保を実現する。

国内の組込みソフトウェア開発の現場における形式仕様記述の適用技術を確立させ、上流工程の品質向上、組込みソフトウェアの高信頼化を実現する
(新技術)
上流工程の作業に数理的な厳密さを保証する形式的仕様記述を導入し、上流工程の段階で不具合の発生を抑制し、品質確保を早期に実現する
(新技術の特徴)
仕様～設計～プログラム実装の間の無矛盾性を数理的に検証し、プログラムの正しさを保証する

・組込みソフトウェア開発への導入試験の実施
‐2件の事例開発(自動車部品制御、通信セキュリティ)を行い、Bメソッドによる組込みソフトウェア設計・開発のノウハウを確立するとともに、上流工程での不具合抑制への有効性を実証した
‐セキュリティ製品の国際規格ISO15408の要求事項を満たす形式手法の適用を、Bメソッドで実現した
・成果普及のための支援ツール・教材開発
‐国内でのBメソッドの技術導入を促進するため、技術者養成用の教育コース、開発支援ツール(ビルド環境生成ツール)などを開発した

・形式手法「Bメソッド」の活用による、数理的に検証された高信頼組込みソフトウェアの受託開発サービス（車載制御、産業通信、IoTシステム等）
・形式手法とBメソッド技術導入のための技術者教育サービス、教材等

・高信頼組込みソフトウェアのニーズを持つ川下企業様との共同で、社内へのBメソッドの技術導入、評価に関する取り組みを進めている
・開発現場の技術者向けに、形式手法とBメソッドに関する技術セミナを開催している(公開セミナおよび個別企業への対応)
・信頼性が求められる機器の開発に研究成果の活用を行う

・欧州産業界での実績
‐Bメソッドは欧州産業界で実績がある形式手法のひとつであり、パリ地下鉄無人運転システムなど多数の実用化事例がある

・テストに頼らない品質の確保
レビューやテストなどの不確実な手段に頼る従来手法ではなく、仕様が設計・実装に正しく反映されていることを数理的な証明により確実に保証する

・上流品質向上でトータルな生産性を改善
‐仕様定義、設計工程の厳密な形式検証と、自動コード生成により、実装後不具合を大幅に削減する
‐検証作業の大部分は支援ツールにより自動化されており、工数増加は最小限に抑えられる

・研究実施メンバ企業各社が、高信頼ソフトウェア開発のニーズを持つ川下企業に対して形式手法の技術導入に関する提案を行い、一部では試作業務の受注を受けている
・本事業からの派生、又は成果活用により、通信セキュリティ(H24～)、農業機械の通信制御(H27～)など複数の技術分野に関する派生研究が実施されている。