ワーキング・グループ

WG3: 形式手法モデリングWG

WGリーダ:中島震 (国立情報学研究所)、佐原伸(CSKシステムズ)

更新情報

[5月19日] 平成22年5月18日までにポジションペーパに基づいてWG参加可否の通知を電子メールでお送りしました。通知を受け取っていない方がいらっしゃいましたら、ポジションペーパ送付先に連絡して下さい。

[5月26日] WG3プログラムが決まりました。

[5月26日] 本WG3へのオブザーバ参加を募集します。オブザーバはポジションペーパを必要としません。シンポジウム参加申込要領にしたがって申し込んでください。

概要

形式手法はシステムに求められる信頼性の達成への技術アプローチとして、産業界からも期待されている。入門的な解説記事や教科書では数理論理に基づくという側面が強調される。数理論理が重要な技術要素であることは事実であるが、実際は、設計方法論やドメイン知識と関連するモデリング技法を含む総合的な技術である。

また、過去に何度か訪れた形式手法ブームとの違いを一言で述べると、今回は、モデル検査に代表されるアルゴリズムベースの自動検証法が実用段階に達したことであろう。しかし、対象システムを有限に限定するなど、利用者が事前に気にすべき作業も多い。特に、抽象化に着目したモデリングが大切な側面になっている。

さらに、形式手法は、ソフトウェア設計に新たなモデリングの規範を導入する技術であるともいえる。形式手法ごとに固有なモデリングの考え方がある。これを習得することが、形式手法の理解につながる。

本WGでは、形式手法とモデリングの関係について、以下の観点から論じる。
(1) ソフトウェア工学で論じられているモデリングと形式手法
(2) 形式手法適用に必要なモデリング(各技法固有、形式手法共通)
(3) 形式手法がもたらした新しいモデリングの規範

参加要件

 ポジションペーパ提出

 形式:pdfファイル、wordファイル(.doc)、テキストファイル、のいずれか

 提出先:ソフトウェアシンポジウム2010投稿先

     ss2010-query [at] sea.jp

 締め切り:2010年5月15日(土)必着

 WG参加可否の通知:5月18日(火)

ポジションペーパについて

 分量:A4判で1~2枚以上

 内容:(1) 今までの形式手法との関わりや経験
    (2) 形式手法モデリングに関する意見や考察
    を中心に、WGで論じたい内容をまとめてください。

 注意:人数の関係等で参加をお断りすることがあります。
    その際、ポジションペーパを参考に決定します。

 WG参加者には採択されたポジションペーパ集を事前に送付する予定です。

WGプログラム(予定)

  • 6月9日 14:15 -- 15:15 (講堂)
    • 荒木啓二郎(九州大学大学院教授):招待講演   
  • 6月10日
    • 10:00 -- 10:30 : オープニング
    • アンケート実施
    • 10:30 -- 12:30 : セッション1「モデリング」
             
    • 中津川泰正、橋本祐介、田端一也、佐原伸
    • 13:30 -- 15:30 : セッション2「パターンとイディオム」
             
    • 石黒正揮、青木利晃、飯田周作、木村浩一郎、只野賢二
    • 15:40 -- 17:30 : セッション3「導入・適用の推進」
             
    • 北村崇師、酒匂寛、早水公二、岡本勝幸
  • 6月11日
    • 10:00 -- 11:30 : セッション4「まとめ」
    • 11:30 : クロージング