【告知】モデル検査

モデル検査の話がSEA関西プロセス分科会で出てくるので展開する。

Wikipediaによると、、

モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。
ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。

モデル検査を使う状況は、特に組み込み系プログラムの設計・テストフェーズが多い。
つまり、プログラムや設計図から状態遷移図を作り、状態遷移図からバグになりそうなアルゴリズムを探し出すというスタイル。
この手法は10年以上前から研究されており、最近のコンピュータ性能の向上から、一部で注目されているらしい。
とはいえ、モデル検査について知見のある技術者は数少ないだろう。

実は、4月のソフトウェア開発技術者試験の午後問題にも、モデル検査が出た。
正直びっくりした。

http://www.jitec.jp/1_04hanni_sukiru/mondai_kaitou_2008h20_1/2008h20h_sw_pm1_qs.pdf

～～　第34回　SEA関西プロセス分科会のご案内　～～

テーマ：動きの設計と検証、さらに自動化

講師　：藤倉 俊幸 （イーソル株式会社）

主催　：ソフトウェア技術者協会 関西支部 プロセス分科会
　　　　　
日時　：2008年05月30日(金) 18:30～21:00

会場　：大阪市立大学文化交流センター
　　　　〒530-0001　大阪市北区梅田1-2-2-600
　　　　大阪駅前第２ビル６階　ホール
　　　　Tel　06-6344-5425　/　Fax　06-6344-5524
　　　　http://www.ado.osaka-cu.ac.jp/BUNKO/　　　

周辺略地図 　　　　http://www.media.osaka-cu.ac.jp/Toshi/yoteiti.html

　　　　※会場の部屋が通常（大セミナー室）とは異なりますので、
　　　　　ご注意ください。（同じビルの同じフロアです。）

内容　：
　　ソフト開発においてはタスク設計が重要です。セミナーでは、
　　モデル検査ツールLTSAについて説明した後、動作要求の仕様化と
　　検証、タスク動作への変換について説明します。手順の概要は、
　　以下の様になりますが、基本的に小難しい話は無しで進めます。

　　1)　動作要求をマインドマップによって表現し、動作仕様を抽出します。
　　2)　各動作仕様をFSP式に変換しLTSAによって実現可能な動作要求セットを作成します。
　　3)　動作要求セットをタスクに分割し、同期構造の設計検証を実施し、タスク設計仕様を作成します。

　　UMLを使用している現場への適用では、動作要求表現として
　　シーケンス図や状態図を利用することで、これらの図からFSP式を
　　自動生成することが可能になります。UMLへの適用に関する詳細は
　　以下のURLを参照してください。

http://www.esol.co.jp/rcs/uml_tool.html

参加費用：
　　SEA正会員：1,000円，SEA賛助会員：1,000円，
　　学生：500円，一般：2,000円

　　定員　：120名

申込方法：
以下のペ‐ジからお申し込みの受付を行っております。
http://www-ise4.ist.osaka-u.ac.jp/K-SPIN/application.html
### 05/28（水）までにお申し込みください ###

　ご注意）
　・受付は先着順で，定員になり次第〆切とさせていただきます．
　　申込受付後のキャンセルは原則としてお断りします．
　・メール，FAXなどWebページ以外からの申し込みは受け付けて
　　おりません．
　・お申し込みの受付け後，確認メールが自動的に返送されます．
　　確認メールを印刷し，当日受付時に持参ください．
　・申し込み手続きについて不明点などございましたら，下記まで
　　ご連絡ください．
　　seakansai-office2007＠media.osaka-cu.ac.jp
　・参加費は当日会場受付にて現金でお支払いください
　 領収書が必要な方は，申し込み時に「領収書要」にチェック
　　してください．