HOME > 活動内容 > 開発支援サービス > 「さつき」による検証サービス

「さつき」による検証サービス

サービス概要

産業技術総合研究所関西センターの連携検証施設「さつき」を利用した数理的技法による検証サービスにより、ソフトウェアの信頼性をアップ！

検証サービス

　検証サービスは、要求仕様や設計仕様、ソースコード、ヒアリング等を元に、モデル検査など数理的技法に基づく自動検査を、産総研で実施するサービスです。主な検査内容は下記のとおりです。

原因不明のバグの解析
仕様書・設計書の検証
ソースコードの検証
テストパターンの自動生成

特長

数理的技法だから

検証対象を厳密に、網羅的に評価するので、微妙なタイミングのずれ等に起因する不具合や発生頻度の低いバグも発見が可能
品質向上と不具合解析の両面でのアプローチが可能
不具合の発見と原因解析が同時に完了

産総研だから

共同研究等で開発の上流工程から下流工程までの様々な段階を対象にモデル検査を実施し多くのノウハウを蓄えているので、状態爆発を抑制するようにモデル作成を工夫して検証できる
大容量メモリ高速演算クラスタと大規模演算クラスタを利用して、従来不可能であった大規模なモデル検査やSAT(satisfiability)手法による検証が可能

振興機構だから

産総研では受け付けられない短期間のプロジェクトでも利用できる
会員特別価格で産総研の検証サービスが利用できる

サービス提供する検証方法

大規模モデル検査

　モデル検査は詳細設計などを計算機上で記述し、その振る舞いを網羅的に自動検査する形式手法の一つです。モデル検査を用いた検査の流れを、上図に示します。
　黒い矢印・文字は、特に人手を介さない処理、赤い矢印・文字は専門の技術者によって行われる処理を表しています。この図が示すとおり、検査自体は自動化されていますが、多くの処理は人手によって行われます。
モデル検査を利用していると、状態爆発は簡単に起こってしまうので、抽象化などにより問題の本質を保ったままモデルを単純化する必要があります。このため、検査ができる適切なモデルを作成するためには、多くのノウハウ・時間を必要とすることがあります。
大規模充足可能性判定
　充足可能性判定機（SATソルバー）は、制約条件を与えると、それらの制約条件をすべて満たす解があるかどうかを判定して、そのような解があれば出力します。
大規模シミュレーションによる検証
　車載システム、家電ネットワーク、制御システムなど、組込みシステムを要素とする大規模ネットワークのシミュレーションのうえで、モデル指向試験を行うことができます。

利用の手順

費用

　連携検証施設「さつき」による検証サービスは、検証対象をモデル検査器にかけるための技術費用、および検証に必要なノード数や利用期間に応じた費用が必要な有料サービスです。機構を利用することで小プロジェクトから安価にご利用いただけます。
　モデル検査の適否など、個々のケースによって大きく異なりますので、まずはお気軽にご相談ください。