SPINコンバータとは
SPINコンバータは、ZIPCで設計したモデルをモデル検査ツールSPINへ容易に変換するためのツールです。
モデル検査って何？
モデル検査ツールに「検査対象のモデル」と「検査したい性質」を入力し、問題が発生しないことを数学的に証明する手法です。
SPINコンバータでは、モデル検査ツールとして広く知られているSPINを対象としております。
SPINコンバータでは、モデル検査ツールとして広く知られているSPINを対象としております。
「検査対象のモデル」って何？
「検査対象のモデル」とは、検査を行いたいモデルのことです。
モデル検査ツールは、ZIPCで書かれた設計書データ（モデル）をそのまま読み込むことはできません。
モデル検査ツールは、ZIPCで書かれた設計書データ（モデル）をそのまま読み込むことはできません。
モデル検査ツールの一つであるSPINは、独自のPROMELA言語を使って「検査対象のモデル」を表現していますので、設計書データをPROMELAへ変換する必要があります。
SPINコンバータは、PROMELAへの変換を素早く行うことができます。
「検査する性質」って何？
「検査する性質」とは、検査したい内容のことです。
例えば、状態遷移表の中に書かれている×(不可セル)は、このセルに来るはずがない、あるいは来てもらっては困る時に記入します。
この場合、「不可セルに来ないこと」ことが検査する性質になります。
SPINコンバータは、不可セルのチェックを「検査する性質」として常に自動的にコンバートします。
例えば、状態遷移表の中に書かれている×(不可セル)は、このセルに来るはずがない、あるいは来てもらっては困る時に記入します。
この場合、「不可セルに来ないこと」ことが検査する性質になります。
SPINコンバータは、不可セルのチェックを「検査する性質」として常に自動的にコンバートします。
他にも、変数の値が常にｘｘ以下であること、等の検査が行えます。
この場合、モデル検査ツールを使って入力する必要があります。
この場合、モデル検査ツールを使って入力する必要があります。
検査した結果はどうなるの？
モデル検査ツールは、検査した結果「検査する性質」が満たされていないときに、反例を出力します。反例に沿って解析することにより、不具合を発見することができます。
結局のところ、SPINコンバータを導入すると何が嬉しいの？
SPINコンバータの特徴は次の４つです。
- 状態遷移表とPromela言語(モデリング)の一致
- 日本語表記の状態遷移表に対応(自動置換)
- 自動変換による生成のため変換ミスが生じない
- 人手変換するとモデルの生成に差異が生じるが、それがない
お問い合わせ
「SPINコンバータVer1.0」のお申し込みは終了致しました。
SPINコンバータについてのお問い合わせは、SPINコンバータセンター（spinconv@zipc.com）までご連絡ください。
SPINコンバータについてのお問い合わせは、SPINコンバータセンター（spinconv@zipc.com）までご連絡ください。
SPINコンバータは第Ⅱ期知的クラスター創成事業の一環として行ったキャッツ株式会社、九州大学、財団法人福岡県産業・科学技術振興財団との共同研究の成果です。