NuSMVによるモデル検査入門 (1) ステートマシンを定義する - Qiita
この前書いた記事はあまりにもやっつけだったので整理してみる。 概要 この記事は、シンボリックモデルチェッカNuSMV (http://nusmv.fbk.eu/) を使って、モデル検査を行うチュートリアルである。 NuSMVのバージョンはv2.6.0とする。バージョンによって機能がobsoleteされたり変更されたりするので、古いバージョン用の資料を読むときには注意されたい。 基礎知識 知ってるならスキップしてください。 モデル検査 (Model Checking) とは 状態遷移系が論理式を満たすかどうかを検査すること。 より正確には、あるKripke構造がある時相論理式を満たすか否かを検査することである。 一般に数理論理学で、データ構造 $M$ が論理式 $\phi$ を成り立たせる場合に $M\models\phi$ と書き「$M$ は $\phi$ のモデルである」と呼ぶことから、
ステートマシン図の設計品質の向上の一手法の紹介
著者：早水公二 (株式会社フォーマルテック)、高井利憲 (チェンジビジョン) みなさんは、astah*で書いたステートマシン図をどのように活用していますか？システムの取り得る状態を把握したり、システムの振る舞いに関する理解を共有したり、不正な状態遷移がないかレビューしたりしていると思います。今回は、モデル検査という技術を応用することにより、ステートマシン図を自動検証する手法をご紹介します。 ■モデル検査の概要 モデル検査とは、システムの網羅的な検査ができる技術です。 網羅的とはどういうことでしょうか。例えば、実機や実際の実行コードを用いる試験やソフトウェアテストでは、特定の環境条件や入力値を設定することによって、検査対象のシステムやソフトウェアの振る舞いを観察します。ただし、一回あたりの試験の実行には、無視できない時間やコストが係るため、限られた環境条件や入力値しか確かめられないのが普通で
NuSMV home page
NuSMV: a new symbolic model checker NuSMV is a symbolic model checker developed as a joint project between: The Embedded Systems Unit in the Digital Industry Center at FBK-IRST The Model Checking group at Carnegie Mellon University, the Mechanized Reasoning Group at University of Genova The Mechanized Reasoning Group at University of Trento. NuSMV is a reimplementation and extension of SMV1, the f
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
