文字サイズ
標準
色の変更

サポイン技術紹介

  1. トップ
  2. サポイン技術検索
  3. 形式的仕様記述を用いた高信頼ソフトウェア開発プロセスおよび開発ツールの確立

情報処理

形式的仕様記述を用いた高信頼ソフトウェア開発プロセスおよび開発ツールの確立

北海道

北海道電子機器株式会社

2020年3月23日更新

プロジェクトの基本情報

プロジェクト名 形式的仕様記述を用いた高信頼ソフトウェア開発プロセスの研究とツール開発
基盤技術分野 情報処理
対象となる産業分野 航空・宇宙、自動車、ロボット、情報通信、スマート家電、半導体、エレクトロニクス
産業分野でのニーズ対応 高性能化(既存機能の性能向上)、高性能化(信頼性・安全性向上)、高効率化(同じ生産量に対するリソースの削減)、高効率化(工程短縮)、高効率化(人件費削減)、高効率化(生産性増加)
キーワード 形式手法、B method、ISO/IEC 15504、機能安全規格
事業化状況 事業化に成功
事業実施年度 平成22年度~平成24年度

プロジェクトの詳細

事業概要

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

開発した技術のポイント

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

形式手法によるソフトウェア設計・開発
具体的な成果

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

研究開発成果の利用シーン

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

実用化・事業化の状況

事業化状況の詳細

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

提携可能な製品・サービス内容

設計・製作、試験・分析・評価、共同研究・共同開発、技術コンサルティング

製品・サービスのPRポイント

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

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

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

今後の実用化・事業化の見通し

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

プロジェクトの実施体制

サポイン事業者 北海道電子機器株式会社
株式会社ミクロスソフトウェア
株式会社ヴィッツ
株式会社リック (現 株式会社LIC)
事業管理機関 地方独立行政法人北海道立総合研究機構
研究等実施機関 株式会社ミクロソフトウェア
株式会社リック (現 株式会社LIC)
株式会社ヴィッツ
国立大学法人北海道大学
地方独立行政法人北海道立総合研究機構
国立研究開発法人産業技術総合研究所
アドバイザー アイシン精機(株)、ルネサス エレクトロニクス株式会社、NECソフトウェア北海道(株)、(株)日本除雪機製作所、トヨタ自動車(株)、名古屋大学、苫小牧高等工業専門学校

サポイン事業者 企業情報

企業名 北海道電子機器株式会社(法人番号:5430001022251 )
事業内容 コンピュータシステム、ハードウェア、ソフトウェアの設計・開発・製造・販売
社員数 20 名
本社所在地 〒065-0010 北海道札幌市東区北10条東10丁目1番1号
ホームページ http://www.hdks.co.jp/
連絡先窓口 システム事業部 穴田
メールアドレス anada@hdks.co.jp
電話番号 011-748-3666