モデル検査とSPIN入門
SEA関西支部プロセス分科会(略称SEA関西SPIN)に参加しました。
トゥルーロジックの野中さんはUNIXカーネルの開発者たちが開発したSPINの解説でした。SPINは状態遷移を検証する処理系で、モデルが取りうる状態と起きてはいけない状態の論理積が空であることをすべての状態を展開して確認します。モデル検証は実装の前に設計を検証するもので、自動、反例を示す、まれにしか起きない問題を検証するといった特徴があります。
言語はPROMELAといい、do-od、if-fiとさすがにUNIXの開発者が作っただけあってshのような表記です。いつかきっとは" <>"、いつもずっとは"[]"、untilは"U"です、このうち、" <>"をひし形はいつかきっと傾くという説明がGOODでした。
モデル検証はアルゴリズムと計算機の高速化で1980年に7日かかったものが今では数秒で処理できるようです。SPINにはモデル検査のCコードを出力する機能もあるそうです。
詳細とツールは、http://www.spinroot.com/にあるようです(私は見れませんでした)。
SRA-KTLの岸田さんは「銀河ヒッチハイクガイド」をつかみに、岸田さんが70年代後半にアメリカのSRAでエドワードミラーと知り合って、カバレージを日本に伝えたお話、LehmanのS(Specificationが定義できる),P(なんとかプログラマブル),E(Embedded)のお話、社会のチリにまみっれているからと大森荘蔵に教えを受けられなかったお話、ソシュールが言語学は規範の額ではない(正しい日本語とか)と同じく、ソフトウェア工学は規範の額ではなく、モデル(文字)はソフトウェア(言語)の正体を隠すものであって、モデルを剥ぎ取ったところに本物のソフトウェアが現れる、E-typeは無限の属性を持つので、仮説は2000年問題のように成り立たなくなる、といったお話で構成されていました。
最後のディスカッションでは、SPINは特定領域に絞って使う、複数の形式手法を組み合わせないといけないのが現状といったわだいが出ていました。
« アジャイルプロセス協議会「西日本セミナー」その3"モチベーションとファシリテーション" | トップページ | お気に入りの一言 »
「パソコン・インターネット」カテゴリの記事
- [Windows10]コア限定で古いソフトを動かす- Wave SplitterでLPのCD化 –(2021.05.05)
- MacBook Air に3,180円で64GB増設 - 安いSDアダプタ発見! -(2016.06.18)
- 買って良かったキーボードPC(WP004)購入記(2016.04.02)
- Twitterはどこへ行くのか?(2015.04.13)
- 簡単すぎるネットワークカメラQwatch - TS-WLCAM -(2013.09.28)
「ソフトウェア」カテゴリの記事
- One fact in one placeとチケット駆動開発 - Software Processes are Software, Too -(2021.12.21)
- マルチスレッド処理と進捗管理・配員・作業分割/割り当て- Software Processes are Software, Too -(2021.12.20)
- カプセル化と組織パターン - Software Processes are Software, Too -(2021.12.20)
- 論文研修会(導入編)- 論理的思考のすすめ -(2019.12.01)
- デブサミ関西でNode-REDとペンギンと勇気の話をしました #devsumiB(2018.10.28)
「プログラミング」カテゴリの記事
- Greedy algorithmと2割8割の法則 - Software Processes are Software, Too -(2021.12.12)
- 論理的に考え伝える – SEA関西「開発現場で役立つ論文の書き方のお話」 -(2021.05.09)
- 論文研修会(導入編)- 論理的思考のすすめ -(2019.12.01)
- スクリプト言語入門 - シェル芸のすすめ - 第2回クラウド勉強会(2019.01.27)
- デブサミ関西でNode-REDとペンギンと勇気の話をしました #devsumiB(2018.10.28)
« アジャイルプロセス協議会「西日本セミナー」その3"モチベーションとファシリテーション" | トップページ | お気に入りの一言 »
コメント