| 活動内容 |
| 【モデル検査によるソフトウェアテストの適用事例・ノウハウ収集と体系化】 |
| モデル検査によるソフトウェアテストは、経験や同種事例から得られるノウハウが非常に有効です。基礎知識だけで取り組むのは、貴重な頭脳と時間のロスが大き過ぎます。そこで、これまでに行ったモデル検査、さらに現在行っているモデル検査によるソフトウェアテストを事例として蓄積すると共に、そこで得られたノウハウを使いやすいように体系化する作業を進めています。また、これまでの適用事例の一部を発表してＰＲに努めています。 |
|
|
| 【モデル検査の実践ノウハウを取り入れた実務者向け教材の開発】 |
| モデル検査の学習に用いる文献は、殆んどが海外のものです。英文の解説や説明書には苦労しました。2004年頃からやっと日本語のセミナーが開かれるようになったのは、素晴らしいことです。セミナー等で基本を学んでいただいた方々が、実務でモデル検査を行われる際に、知っておけば無用な苦労を防止できる実務ノウハウを盛り込んだガイドブック・教材を開発しています。 |
|
|
| 【モデル検査支援ソフトウェアの開発】 |
| モデル検査では、モデル検査専用のプログラミング言語を用いて検査対象を記述します。プログラマーにとっては、難しいものではなく、演習問題や小さなシステムでは問題ありませんが、実務としてモデル検査を始めると「モデル検査のプログラミングをなんとかしてくれ。我々の目的は検査プログラミングでなくてソフトウェアのテストだぞ」「反例が出てきたけれど見難くて大変」と言った声が出てきます。そこで、支援ソフトウェアを開発中です。プログラマー以外の人にも便利です。 |
|
|
| 【大規模システム検証用64bit版モデル検査器の開発】 |
大規模システム検証用の64bit版モデル検査器を、基本設計から始めて新規開発しました。
64bitOSに対応することで、利用可能なメモリ領域を大幅に拡大しました。
従来の32bit版で発生していた状態爆発を回避できる可能性が高くなります。データ構造としてはBDD（Binary Decision Diagram）を採用しています。
CTL（Computation Tree Logic）式で記述した検査項目を検査することができます。 |
|
＜64bit版モデル検査器で検査できるSMVファイルについて＞
64bit版モデル検査器で検査できるのはNuSMVのSMVファイルのサブセットです。モデルを記述する専用言語は、NuSMVのモデル記述言語の構文の一部を採用しています。検査項目記述部ではCTL式を記述することができます。
「大規模システム検証用64bit版モデル検査器のSMVファイルについて」をご参照ください。 |
|
|
|
