第８回 teNet ワークショップ
| 第８回 teNet ワークショップ | |
|---|---|
| テーマ | 形式検証のソフトウェア検証への応用 |
| 講演者 | 早稲田大学 理工学術院 創造理工学部 経営システム工学科 教授：岸知二先生 |
| 当日の朝の風景 | |||
|---|---|---|---|
|
|||
| ワークショップ中の風景 | |||
ご講演中... |
みんな真剣です |
||
| 休憩中の風景 | |||
ちょっとだけ |
休憩です |
||
| ご講演再会 | |||
みんな |
真剣です |
質疑応答中 |
|
| 懇親会の風景 | |||
こんな |
感じです |
||
参加者からのコメント
■A.N
形式手法や形式検証は、本やWebなどの「読み物」からでは抽象度が高く、 入門しずらいが、今回の岸先生のご講演はそんな敷居を外してくれたほど わかりやすいものだった。例題がとても理解しやすい内容だったのかもし れないが、実際に定義を行う際、どのような内容を、どのくらい定義する のかなどを実例を持って示していただいたおかげで、「ボリューム感」を 掴むことが出来た。また、「形式検証だけで、検証作業が全て網羅できる のだろうか．．．」という自分なりの感想も、岸先生は「検証作業を全て 形式手法で行うのではなく、他の検証方法と組み合わせて使用するのが現 実的」と言っていただいたので、心のモヤモヤが晴れた気がしました。
■Y.Y
今回のテーマである形式手法・形式検証は、 今までまったく知らない分野でした。事前に 調べようと、インターネットで検索してみま したが、難しい数式がでてきたりと、やはり とっつきにくいものでした。しかし岸先生の ご講演では、具体的かつ簡単な事例をもって 実演していただき、また形式検証の現在の課 題なども隠すことなく教えて頂き、実際に形 式検証を行なうイメージがもてました。
■Y.H
形式手法についてや形式検証技術をどうソフト開発に活用するか、 さらには、事例やツールを使いながらどのように検証するかなど 具体的な事例を交えデモが行われた。また、設計検証のメリットや 利用上の留意点についてもご説明され、とても分かりやすく理解する ことができた。当社ではソフト開発における検証方法はレビューや テスト主体であるが、形式検証のモデル検査という検証方法を取り 込むことで、設計段階では正確性や厳密性の求められる機能の 検証ができたり、実装工程ではアーキテクチャや実装方式の検証が できるため、よりよい製品開発につながる可能性があることが分かった ことは非常に良いワークショップであったと思う。
