4/29に第4回FormalMethods勉強会を行いました。
今回は
Alloy
Alloyの教科書の例題（アドレス帳）を元に文法を勉強しました。大体文法は把握出来たかな。
あとは自分で使ってみるべきなんだろうが、あまりモデリングとか仕事でやらないしなぁ。とりあえずパズルをAlloyで解く練習をするかなぁ。
CEGAR
今回はCEGARという手法の話を聞きました。CEGARはCounterExample-Guided Abstraction Refinementの略で、モデル検査における状態数爆発を抑える為の一手法です。
モデル検査で扱う検査の中に、到達可能性解析（エラー状態などの特定の状態にと到達するか否かの解析）があります。
状態数を抑える方法としてモデルの抽象化（モデルの粗視化）があります。抽象化によって、エラー状態に遷移する可能性のある状態と、到達しない状態とが同一視されてしまうと、本当はエラー状態に到達しないにも関わらず、エラー状態に達すると誤って判定されます。
CEGARは、エラー状態に到達する解に対して、解析（最弱事前条件？）を行って抽象化を修正（状態を分割）して再解析する手法です。エラー状態に達した場合にはそれが本当に達したのか、抽象化を改善して再度解析を実施します。
原理だけ聞くと、当たり前の話と思えるのですが、実際に自動化するところを実装するのは難しそうというか見当が付かない。
Coq
CoqはCertified Programming with Dependent TypeのChapter 1,2をざっと流して、Chapter 3を3.3まで読み終わりました。
当日使用した資料 (PPT, Coqファイル) についてはGoogleグループ上の記事にリンクを纏めましたので、そちらから辿って下さい。
本当はChapter 3を終わりたかったのですが終わらなかったのはちょっと残念でした。
No comments:
Post a Comment