「モデル検査によるソフトウェアテストの実践研究会」は，産業技術総合研究所（産総研）と協力し、同研究所の演算クラスタを利用してモデル検査（プロパティ・チェッキング）をネットワーク上から実行できるオンライン・サービス「64ビット版モデル検査器によるモデル検査サービス」を実施している（同サービスのサイト）。産総研の関西センターが運用・管理する「連携検証施設 さつき」の「大容量メモリークラスター」を利用しており、主記憶容量が1Ｔバイトおよび256Gバイトの演算資源をモデル検査向けに無償で利用できる。 一般にモデル検査では，入力したモデルの状態遷移をしらみつぶしにチェックするため，探索空間が大きくなりすぎる「状態爆発」をいかに避けるかが課題だが，1Tバイトと非常に大容量な主記憶を利用することで探索可能な空間を拡大し、状態爆発を避けやすくなる。
この記事は会員登録で続きをご覧いただけます
-
会員の方はこちら
ログイン -
登録するとマイページが使えます
今すぐ会員登録（無料）
日経クロステックからのお薦め
日経BP 総合研究所がお話を承ります。ESG／SDGs対応から調査、情報開示まで、お気軽にお問い合わせください。
ブランド強化、認知度向上、エンゲージメント強化、社内啓蒙、新規事業創出…。各種の戦略・施策立案をご支援します。詳細は下のリンクから。
「デジタル＆ソリューション」をキーワードに、多様な事業を展開しています。
日経BPは、デジタル部門や編集職、営業職・販売職でキャリア採用を実施しています。デジタル部門では、データ活用、Webシステムの開発・運用、決済システムのエンジニアを募集中。詳細は下のリンクからご覧下さい。
