技術座談会は、OACISの活動の一つとして、特定のテーマをとりあげ、大阪大学情報科学研究科とOACIS参加企業の連携について自由な議論をする場を提供するものです。これまでに50回を超える技術座談会を開催し、産学連携を生み出すきっかけなどの役割を果たしてきました。過去の参加者の声を反映し、今年度より、1つの技術座談会あたりのトピックを1テーマに絞る一方で、講演時間を長く設定することで、より深くより密な議論ができる実効的な会合を目指しています。
今回、第{{ num }}回技術座談会では、{{ labs[0].long_name }}（{{ labs[0].short_name }}）により、「{{ title }}」をテーマとした座談会を開催します。興味をお持ちの方々に足を運んでいただき、情報科学技術におけるホットな技術を通して、情報科学研究科とのつながりを深めていただけることを願っております。
講師
- 大阪大学 大学院情報科学研究科 {{ l.department }} {{ l.long_name }}
- {{ s.position }}・{{ s.name }}{{ s.name }}
内容
{{ t.title }}
本講演では、モデル検査と、その自己適応システムへの応用について説明します。
モデル検査とは、システムの設計の正しさを機械的に検証する手法です。システムが取り得る状態を網羅的に探索することで、極めて限られた動作でしか現れないエラーについても、発見することが可能です。
講演の前半では、モデル検査の基本概念とツール、および、応用事例について紹介します。ツールの例としては、SPINとCBMCを取り上げます。SPINは最もよく知られたモデル検査ツールで、通信プロトコルや車載ソフトウェア等の検証に広く応用されています。また、CBMCはCプログラムを直接検証することができるだけでなく、一般的なテストと違って、あらゆる入力に対する動作を検査することが可能です。これらのツールについて、簡単な例を通じて使い方を説明するとともに、研究室の事例も含めた応用事例について紹介します。
後半では、自己適応システム実現に向けてのモデル検査の応用事例について紹介します。自己適応システムとは、環境に適応するために自らが振舞いを決定し変更するようなシステムであり、決定した振舞いの有効性を確認するために、モデル検査の実行時適用が期待されています。特に、環境の不確かさを表現するために、確率的モデル検査が着目されています。後半部では、自己適応システムと確率的モデル検査について概説し、自己適応システム実現に向けての確率的モデル検査の応用事例について紹介します。
開催日時
{{ date }}
開催場所
参加方法
参加対象
- IT連携フォーラムOACISの会員企業・団体に属する方および参加希望企業の方
- 大阪商工会議所の会員企業・団体に属する方および参加希望企業の方
参加費用
無料参加登録締切
{{ deadline }} （参加登録は締め切りました）
報告書をこちらからご覧になれます。
運営
主催
共催
問い合わせ先
座談会内容に関する問い合わせ先
大阪大学 大学院情報科学研究科 {{contact.department}}
{{contact.name}} ({{contact.address}}
)
報告書
| 開催日 | {{date}} |
| 開催場所 | Zoom meeting |
| テーマ名 |
|
| 講師 |
|
| 参加人数 |
|