モデル検査の講演会を聞いてきました

名古屋工業研究所さん主催の講演会を聞いてきました。

状態遷移をきちんと考えてちゃんとしたモデルを考えていれば、それを検証用の言語に落として総当たり的に検証することは充分可能で効果もあるよ、というお話しでした。
ハード屋さんやファーム屋さん、組込み系の方は、コンピューター・システムを状態モデルとしてとらえるのが普通かもしれませんが、ある層より上に乗っているところのソフト屋さんはコンピューターをプロセッサとして捉えていて状態遷移をあまり考えません。だからモデル検査もピンとこないところがあるんだと思います。僕も今までほとんど状態遷移図は描いたことなかった。でも今回いろいろと勉強になったのでこれからは意識して状態考えて、できればモデル検査もトライしてみたいです。

講演会とセットでライトニングトークス大会が開かれました。僕も5分程高橋メソッドで話したのですが、うーん、やっぱり技より心ですよこういうのは。他の発表者のみなさんのお話はどれもよかったです。足立さんはやはりさすが。富士ゼロックスの山本さんの話もよかったです。レガシーコードの複雑さを循環的複雑度のグラフでバシっと表現して、SPINでCharacoristic Testを自動生成しちゃうよなんて話で引きつけておいて、結論は飲みにいきましょう皆さん、と落とすなんて。

講演会の後の懇親会では足立さんや他の方々とお話しできてよかったです。