モデル検査

スクリプト言語へのモデル検査のサンプルプログラムを書いてみた

「モデル検査のゲームシナリオへの適用」にて、モデル検査を実開発に適用するのための基本の基本の部分を説明し終わりましたので、実際に、説明用の超簡易スクリプト言語へ、説明したモデル検査手法を適用してみるサンプルプログラムを作ってみました。まず…

中島震「SPIN モデル検査」近代科学社

先日の CEDEC のセミナーで NII の石川先生が勧めていらっしゃった書籍をさっそく買ってみました。タイトルどおり、SPIN というモデル検査ツールの本なのですが、SPIN のツールとしての使い方で終わっていないのがよいですね。簡単なモデル検査の概論から、S…

「モデル検査のゲームシナリオへの適用」を執筆中

夜行バスで無事に帰ってきました。昨日のモデル検査のセッションはおつかれさまでした。昨日のモデル検査のセッションと関連して、「モデル検査のゲームシナリオへの適用」というページを執筆中です。モデル検査の技術のうち、ゲームのシナリオスクリプトへ…

モデル検査のセッション@CEDEC

セッション概要が公表されましたが、今年の CEDEC (CESA Developers Conference) にて、「モデル検証入門〜ツールに振る舞いを検査させる〜」というセッションが「CEDECラボ」の1つとして行われます。「CEDECラボ」は、ゲーム研究などの学術界と、ゲーム開発…

FF4DS のお客様にご迷惑をおかけする「現象」

DS 版の Final Fantasy IV で2件の「現象」が見つかっているという案内が出ています。一件目は、2週目以降においてイベント回想モードで「未来へのプロローグ」(エンディングの一場面)を観てしまうと、その後、本物のエンディングの途中で先に進まなくなる…

「モデル検査ツールUPPAALを使った時間制約の検証」のご案内

id:sumii 経由で知りましたが、日本ソフトウェア科学会による、モデル検査がらみの以下のレクチャーがあるそうです。 「モデル検査ツールUPPAALを使った時間制約の検証」 2007年11月16日(金) 午前10時30分〜午後5時(受付開始:午前10時) 国立情報学研究所 …

無償で使えるソフトウェアモデル検査の体験ツール

ひょんなことから知ったのですが、「モデル検査によるソフトウェアテストの実践研究会」という団体が 「実践!ソフトウェアモデル検査」 というサイトを作っていたんですね。モデル検査というとついつい理論的な研究が先行しがちですが、ここでは名前通り実…

"Model Checking" の日本語解説

http://www.ueda.info.waseda.ac.jp/~shibuya/pukiwiki/index.php?Model%20CheckingClarke 先生の "Model Checking" を題材とした輪講で用いられたと思しき資料が上記の Wiki にありました。あまりにも素晴らしく、感動しましたのでメモ。これで、あまりにも…

Systems and Software Verification

前掲の本と一緒に購入したのがこの洋書です。どこかで紹介されていたので、ふとした気まぐれで購入してみたのですが、これが大当たりでした。Clarke 先生の "Model Checking" は内容がぎっしり詰まっているため、理解しながら読み進めるのにかなりのエネルギ…

4日で学ぶ モデル検査

ずいぶん前に購入していたのですが、忙しくて感想を書けていませんでした。結論としましては、ツールとしてのモデル検査に興味がある方には実践的かな、と。モデル検査の代表的なツールである NuSMV と SPIN の両者で、さまざまな演習課題を解いてみる、とい…

Clarke 先生の講演@計算機言語談話会

大阪の千里にある産業技術総合研究所のシステム検証研究センターでは、隔週くらいの頻度で計算機言語談話会というものが開かれています。モデル検査や対話型定理証明の講演を無料で聞くことができるというありがたいイベントですが、平日の昼間に開催という…