2012年5月14日2012年5月14日 5 Comments
ESEC2012
先週、ESECに行ってきました。
ちょっと形式手法について気になっていたので、専門（＝有料）セミナーを受講したのですが、ちょっと面白い話を聞けました。
というのも、個人的に形式手法なんて実用化はまだまだ先だと思っていたのですが、講師の先生いわく「適用方法がまずいからそうなる。こういう風にやれば、もっと問題をシンプルに出来る」との事。
ものすごくはしょっていうと「外から内へ」。すなわち、システム内部で持ってるプロパティ（＝性質）なんかは後回し。とにかく外から見えるプロパティだけさっさと定義しちゃえばいい。そうするとプロパティ検証もぐっと楽になる、と。
話だけ聞いているともっともらしいのですが、きっとそれは抽象化のワナ。個人的にグッとくる話ではありますが、実業務に落とし込もうとすると何が起きるか分かりません。たまたま運よく、検証手法開発のプロジェクトに関わらせて頂いているため、上記のコンセプトがホントに使えるのかどうか、試してみるつもりです。
同じESECのこちらの講演で、
「MBD(Model Based Development）上級者を目指す為の状態遷移の正しい使い方と、
Simulink構造化技術について」
シナリオとして作った状態遷移と、実装の状態遷移を区別にせずに、
シナリオを形式検証しても無駄と言ってましたよ。
シナリオは、ユースケースの代表例が記載されているだけで、形式検証の意味がない。
どうしても、プロパティ検証がしたいなら、
SimulinkやStateflowの実装状態に持ってきて、SLDVで検査したほうが良いです。
ミーリーの持っている意味論では、実装状態の表現ができないので、
必要な情報が抜けたり、全部入れると状態を最適化できず、破綻します。
ハレルチャートを上手に使えば、そもそも形式検証を必要とするような大きなモデルになりません。
コメントありがとうございます。参考になります。
私の中で検証というと、ざっくり「何を確かめるために」「どの対象を」「どのような方法で」検証するのか？という区分があります。
コメントいただいたのは「どの対象を」という部分ですね。状態遷移に限って言えば、とっととStateflowにしてしまえというのは、なるほどなぁと思います。ミーリーとハレルチャートの（運用上の）区別がイマイチ分かっていないのでアレですが、ハレルチャートを上手に使えば、そもそも形式検証すら要らないというのは、すっごく気になります。検査対象をシンプルにするというのは、何よりも重要に思えますので。
とは言え、具体論なしで話をしていても空中戦になっちゃうんですよねぇ。こういう議論が出来る方と出会えるチャンスが少ないので、すっごく残念です；；
もうちょっと勉強をして、具体的な話をだしながら色々と議論できたらいいなぁ、と思っています。
今後ともよろしくお願いいたします
JMAABのサイトに、2011年のオープンカンファレンスがあり、
その資料に状態遷移図の最適化事例が掲載されています。
ESECはお金が必要でしたが、メンバー登録すれば無料でダウンロードできます。
状態として扱えるのは、有限数で示される物です。
最初に有限オートマトンですから当たり前です。
にもかかわらす、無限数となる”記憶”を状態として扱うと、状態爆発が起きる。
自動販売機の例で、お金やジュースの種類で状態遷移を書いたものはシナリオ。
そもそも、お金やジュースは記憶なので、そのまま制御として使用する状態ではない。
シナリオから、動作基点でまとめると、正しい状態が抽出されます。
フリップフロップを状態遷移図で示したのは使い方、
または意味論を示した例題です。
そもそもフリップフロップは記憶を扱っています。
状態遷移としての正しい例題ではないのです。
アドバイスありがとうございます。JMAABさっそく登録申請してみました。登録が完了したら例題を見てみます。
（むかーし登録したような記憶があるのですが、ユーザーIDやらパスワードやらサッパリ覚えていません。登録したのかどうかも怪しいという、ボケボケ状態です。いけませんね…）
JMAABの資料、読みました。久保様が発表されたものですね。
検証の対象となるモノ（状態遷移図とか）を、どのように書けばシンプルにできるのか？という目線でみてみました。
最初にミーリーマシンとして紹介されていた、自販機にコインを入れていく様をモデリングする際に「５０円投入状態」「１００円投入状態」…といった状態を作っていく件、これをそのまま検証対象とするのは、そもそも論外という印象をうけました。
ソフトに落とし込める状態遷移図（ハレルチャート）を書くため、さいしょにちょっとラクガキしてみました、というのであれば理解できます。しかし、これを「満たすべき仕様書だ」と考えて、その仕様に矛盾が無いのか形式検証してみましょう、という話にはならないというか、なったら怖いですね。
その点で、ESEC情報様や、久保様には完全に同意です。
ただ、こういうウッカリチャート（５０円投入状態、１００円投入状態…）をそのまま検証しようとする事も、現実にあるのかも分かりませんね。これはこれで、気をつける必要はありそうです。
ちなみに、ボデー系なんかだと、まじめにハレルチャート書いてもかなり複雑になっちゃいますので、それをシンプルに出来る魔法のメソッドでもあるのかなーなんて微妙に期待してみましたが、さすがにムリっぽいですね。（世の中、あまくない！）
フリップフロップを状態遷移の例題する件については、「フリップフロップの何を見たいのか？」によって変わってくると思います。
フリップフロップを単に「１ビット記憶子」としてみるのであれば、おっしゃるとおり、この状態遷移図でいったい何がしたいの！？と叱られちゃいます。
一方、「えっ？ゲートを組み合わせることで記憶子が作れる？いったい、どうやってやるの？」という動機から、フリップフロップの動作原理をわかりやすく図示したいという目的であれば、これを状態遷移図で表すのはとても良い方法と思います。
ESEC情報様のおっしゃるとおり、このあたりを混同すると痛い目にあいそうなので、やっぱり注意が必要ですね。
色々と、勉強になりました。ありがとうございます。