HOME>サービス>サービスの概要

サービス

サービス概要

サービス

  検証サービスは、要求仕様や設計仕様、ソースコード、ヒアリング等を元に、モデル検査など数理的技法に基づく自動検査を、産総研の研究員が支援するサービスです。
  モデル検査を用いた検査の流れを、図4に示しました。黒い矢印・文字は、特に人手を介さない処理、赤い矢印・文字は専門の技術者によって行われる処理を表しています。この図が示すとおり、検査自体は自動化されていますが、多くの処理は人手によって行われます。
  モデル作成において、モデル化言語が直接提供しない機能を扱えるようモデルの作成法を工夫する必要があったり、検査が計算機で扱えるサイズをこえないように、一部問題を単純化する必要があったりします。モデル検査を利用していると、状態爆発は簡単に起こってしまうので、抽象化などにより問題の本質を保ったままモデルを単純化する必要があります。このため、検査ができる適切なモデルを作成するためには、多くのノウハウ・時間を必要とすることがあります。


これまで産総研では、共同研究等で開発の上流工程から下流工程までの様々な段階を対象にモデル検査を実施し、ノウハウを蓄積してきました。また、クラスターシステムの導入により、より大きな問題・より短時間で検査できる体制を整えてきました。 主に、次に挙げる内容についての検査を支援することができます。

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

モデル検査が適している・適していないなど、個々のケースによって大きく異なりますので、
まずはお気軽にご相談ください。

▲ページ先頭へ

クラスター利用サービス

クラスター

  HaaS (Hardware as a Service) 型のサービスとして表1のクラスターシステムを有償でご利用いただけます。ハードウェア・ソフトウェア開発などをより効率化することや、ネットワークの実証実験、社会の安心・安全を図るのに必要な技術の開発・適用、テスト、検査・検証などのためにご利用していただき、産業の健全な発展に貢献することを目的としています。


◆表 1 各クラスターシステムの仕様

グループ CPU メモリー容量
(総容量)
ノード間
接続
台数 CPU数
A Intel Xeon X5260 3.3GHz
Dual Core × 1
8GB
(896GB)
1Gbit
Ethernet
112 224
B Intel Xeon E5450 3.0GHz
Quad Core × 2
24GB
(384GB)
1Gbit
Ethernet
16 128
C Intel Xeon E5450 3.0
GHzQuad Core × 2
48GB
(768GB)
1Gbit
Ethernet
16 128
      144 480

グループ CPU メモリー容量
(総容量)
ノード間接続 台数 CPU数
X AMD Opteron 8222
3.0GHz Dual Core × 8
256GB
(7TB)
10Gbit
Ethernet
28 448
Y Intel Xeon X73502.93GHz
Quad Core × 16
1TB
(3TB)
10Gbit
Ethernet
3 192
      31 640

 表中のメモリー容量は、それぞれ1台で使用できる共有メモリーの容量となります。この範囲内であれば、特にプログラムを修正することなく、1つのプログラムで全容量を使用することができます。産総研の提供する基本環境では、Debian Linux 5 を使用できますので、Linux のご利用経験があれば、すぐにご利用いただけます。また、複数台を使って1つのソフトウェアを実行する場合は、MPIなどの並列分散技術を導入することでご利用いただけます。



▲ページ先頭へ