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

id:sumii 経由で知りましたが、日本ソフトウェア科学会による、モデル検査がらみの以下のレクチャーがあるそうです。

 「モデル検査ツールUPPAALを使った時間制約の検証」
 2007年11月16日(金) 午前10時30分〜午後5時（受付開始：午前10時）
 国立情報学研究所 12階会議室

UPPAAL というモデル検査ツールを使用した検証方法を教えてもらえるようです。一般非会員で12,000円。詳しくは: http://www.topse.jp/tutorial/UPPAAL-tutorial-20071116.html

UPPAAL のインストール方法が載っていますが、ダウンロード前にいろいろ入力しないといけない項目が多くて諦めました。説明文によると、時間の制約を検証できるのが、組み込みソフトウェア向けなのだとか。モデル検査用語でいうと、timed なんとか、と言われるタイプの検証を行えるツールなんでしょうね。

追記

日本語訳されたUPPAALのチュートリアル(PDF)を発見したのでざっと読んでみましたが、Java 上で動く GUI を使って、モデルを入力することもできるモデル検証ツールのようです。時間は連続で、ガードで使われる場合はリージョンとしてシンボリックに扱われます。あとは、並行プロセスは独立した状態遷移機械として表現され、プロセス間通信は a! と a? のペアが同時に発火する感じで同期的に行われる模様。どのくらい実用になるかは触ってみないと何とも言えませんね……。