(sigemb-info 114) Workshop on Formal Method

[SAWADA Atsushi <sawada@xxxxxxxxxxxxxxxxxxx>]

IPSJ SIGEMB の皆様，京都大学の沢田です．

12/1にNIIで開催されます形式手法ワークショップのご案内をさせていた
だきます．(重複してお受け取りの方はご容赦ください)

--
        沢田篤史＠京都大学 学術情報メディアセンター 研究開発部
        e-mail sawada@xxxxxxxxxxxxxxxxxxx

----------------------- 8< -------------------------

「形式手法ワークショップ」へのお誘い

○　日時と場所

　　日時：平成１８年１２月１日（金）１４：００−１８：００
　　場所：国立情報学研究所　１２階　１２０８・１２１０会議室

    ### １３：４０開場

○　主旨

　　形式手法への関心が高まっており、商業誌(*)でも取り上げられている。
　　しかし、４０年あまりにおよぶ研究の蓄積があることが逆に災いして、
　　形式手法の全体像を把握することが難しい。その結果、どのような技術
　　であるかが正しく伝わっていないことが多い。

　　一方、形式手法の技術自身も、その歴史的な発展の中で姿を変えている。
　　最近ではモデル検査法が国内でも使われ始めている。さらに、1990年代
　　中ごろから、簡易形式手法と呼ぶ考え方が提案され、対象をうまく選べば
　　自動検証を可能とするツールが開発されている。

　　形式手法を使う・使わないに関わらず、形式手法とはどのような技術で
　　あるかを知っておく時期に来ている。さらに、「形式手法は使えるか」、
　　ではなく、「どのように使えば形式手法は有効か」を考える段階であろう。

　　今回、チュートリアルとパネル討論を中心に、形式手法に関心のある方々に
　　よる議論の場を持つことを企画した。チュートリアルによって現状を紹介し、
　　パネル討論によって形式手法を適用する際に遭遇する問題点を整理することを
　　意図する。また、聴講参加の方々からの活発な議論を期待している。

    (*) たとえば、日経エレクトロニクス　平成17年12月19日号
　　　　　　　　　　（同上）　　　　　　平成18年８月28日号
　　　　　　　　　日経コンピュータ　　　平成18年７月24日号

○　プログラム

　　第Ⅰ部　チュートリアル（１４：００−１５：３０）

　　　簡易形式手法 (Lightweight Formal Methods, Formal Methods Light)　と
　　　総称される手法に関して、提案された背景を説明し、代表的な方法である
　　　モデル検査法、拡張静的チェッカ、の概要を紹介する。

　　　また、最近の研究動向について、本年８月から１０月に開催された幾つかの
　　　国際学会・シンポジウムでのトピックスを紹介する。

　　　司会：　鵜林　尚靖（九州工業大学）
　　　講師：　中島　震（国立情報学研究所）


　　第Ⅱ部　パネル討論（１５：４０−１７：５０）

　　　形式手法の分野で活躍する若手の研究者ならびに産業界で長く形式手法に
　　　関わってきた技術者を招き、以下のような観点を含めて議論する。

　　　　−　形式手法をどのように使えば有効か？
　　　　−　必要な基礎知識は何であって、どのようにして身につければ良いか？
　　　　−　大学教育と企業内教育の役割分担は？

　　　司会：　沢田　篤史（京都大学）
　　　パネリスト：（五十音順）
　　　　　　　青木　利晃（北陸先端科学技術大学院大学）
　　　　　　　飯田　周作（専修大学）
　　　　　　　来間　啓伸（日立製作所システム開発研究所）
　　　　　　　佐原　伸　（ＣＳＫ）
　　　　　　　松本　充広（福岡知的クラスター研究所）

○　参加

　　準備する会場の都合もあって参加者数を事前に把握するため、
　　下記、「問合わせ先」まで、聴講参加希望の旨を連絡。（参加は無料です!!）

○　企画

　　国立情報学研究所アーキテクチャ科学研究系
　　情処学会ソフトウェア工学研究会組込みソフトＷＧ
　　ＩＰＡ・ＳＥＣ

○　問合せ先

　　国立情報学研究所アーキテクチャ科学研究系
  　中島　震       nkjm AT nii DOT ac DOT jp