DSW'08summer

第6回ディペンダブルシステムワークショップ（DSW'08summer） †

第6回ディペンダブルシステムワークショップを以下の通り開催致します。皆様の論文投稿ならびにご参加をお待ちしております。

日時	2008年7月2日（水）～4日（金）
場所	函館大沼プリンスホテル
主催	日本ソフトウェア科学会ディペンダブルシステム研究会
共催	産業技術総合研究所システム検証研究センター

前回より合宿形式にして、完成された仕事の発表よりも、アイディアの交換を重視するディスカッション中心の会となるよう企画しました。とくにシステム開発の分野と検証技術の分野の研究者が研究上の交流をはじめるきっかけの場となるよう期待しております。

そのため、参加者全員に発表（通常の研究発表あるいは5～10分程度のポジション発表）をしていただくことにいたしました。また、ワークショップでの発表を発展させて、完成された発表につなげていただきやすいよう、秋に第5回「システム検証の科学技術」シンポジウムの開催を企画しているほか、論文を投稿いただきやすいよう、コンピュータソフトウェアの特集号を企画中です。

↑

企画講演 †

今回のワークショップでは以下の企画講演を予定しています。

↑

招待講演 †

佐野範佳氏（豊田中央研究所）
「組込みシステムにおける形式的手法の実用化に向けて：車載システムを題材とした課題検討」
篠田陽一氏（北陸先端大）

↑

「システム検証の科学技術」シンポジウム特別講演 †

「システム検証の科学技術」シンポジウムにおける実際的な事例から本ワークショップと関連の深いテーマについてご講演いただきます。シンポジウムからさらに発展した内容を含めてご講演いただく予定です。

高橋和子氏（関西学院大学）
「モデル検査器SPINによる船舶用システムのモデル化と検証」

藤倉俊幸氏（イーソル株式会社）
「オーバーラップ制御の設計と検証」

↑

プログラム †

フルペーパー(F) （発表 20 分、質疑 10 分）
ショートペーパー(S) （発表 15 分、質疑 5 分）
ポジションペーパー(P) （発表 10 分、質疑 5 分）

↑

7月2日（水） †

14:45-14:50 オープニング

14:50-15:50 招待講演　（座長：木下佳樹 (産総研)）

・組込みシステムにおける形式的手法の実用化に向けて：車載システムを題材とした課題検討
  佐野範佳 (豊田中央研究所)

15:50-16:05 休憩

16:05-17:25 モデル検査　（座長：高田喜朗 (高知工科大)）

・モデル検査における反例集合のオートマトンによる表現とその獲得法(F)
  中野昌弘, 高井利憲 (産総研)
・モデル検査器とデバッカの組合せ(S)
  永藤直行 (立命館大)
・モデル検査器を用いた依存型システムのための配列境界の推論(F)
  野尻隆宏, 前田俊行, 米澤明憲 (東大)

17:25-17:40 休憩

17:40-18:30 システム開発　（座長：河野健二 (慶大)）

・安全かつ拡張可能なOS開発基盤実現に向けて(S)
  藤田肇, 平野貴仁, 松葉浩也, 前田俊行 (東大), 菅谷みどり (JST), 石川裕 (東大)
・大規模ウェブアプリケーション開発支援ツールの提案(P)
  福田浩章 (慶大)
・分散ECUシステムの開発手法(P)
  渡邉晃, 青山昌寛 (日産)

19:00-      夕食

↑

7月3日（木） †

 9:15-10:15 招待講演　（座長：木下佳樹 (産総研)）

・タイトル未定
　篠田陽一 (北陸先端大)

10:15-10:30 休憩

10:30-11:50 検証　（座長：高井利憲 (産総研)）

・Continuation based Cによる組み込みシステムの自己検証(F)
  河野真治 (琉球大)
・様相論理を用いた検証手法の並行ごみ集めへの応用(S)
  田辺良則 (東大), 高橋孝一 (産総研)
・多重文脈自由文法の自動検証への応用について(P)
  関浩之 (奈良先端大)
・書類の定式化と検証(P)
  木下佳樹 (産総研)

11:50-13:20 昼食

13:20-14:20 シンポジウム特別講演　（座長：木下佳樹 (産総研)）

・モデル検査器SPINによる船舶用システムのモデル化と検証
  八尾俊佑 (関西学院大学), 粟野宏昭, 平岡康 (古野電気), 高橋和子 (関西学院大学)
・オーバーラップ制御の設計と検証
  藤倉俊幸（イーソル株式会社）

14:20-14:35 休憩

14:35-15:50 モニタリング　（座長：河野真治 (琉球大)）

・リソースモニタリングによる異常検出システム(S)
  大野有輝, 権奇徳 (早大), 菅谷みどり (JST), 中島達夫 (早大)
・要求違反の実行時監視と原因診断(S)
  中島震 (NII), 鵜林尚靖, 外村慶二 (九工大)
・ネットワーク管理システムにおける状態収集機構(S)
  酒井将人, 藤田肇, 松葉浩也, 石川裕 (東大)
・携帯電話におけるソフトウェア実行ログの記録手段に関する検討(P)
  藤本拓 (NTTドコモ)

15:50-16:05 休憩

16:05-17:25 高信頼　（座長：前田俊行 (東大)）

・ディスク故障下におけるオペレーティングシステムの起動保証(F)
  田井秀幸, 山田浩史, 河野健二 (慶大)
・ハイブリッドシステムの高信頼シミュレーションへの区間ニュートン法の適用(S)
  石井大輔, 上田和紀 (早大), 細部博史 (NII)
・仮想機械技術を用いたソフトウェア若化の高速化手法(F)
  古林隆宏, 山田浩史, 河野健二 (慶大)

18:00-      懇親会

↑

7月4日（金） †

 9:15-10:30 言語・プログラミング　（座長：関浩之 (奈良先端大)）

・SMP・マルチコアに対応した型付きアセンブリ言語(F)
  前田俊行, 米澤明憲 (東大)
・組み込み向け低レベル言語 CbC の GCC による実装(F)
  与儀健人, 河野真治 (琉球大)
・通信指向プログラミングによる高信頼ソフトウェア設計(P)
  結縁祥治 (名大)

10:30-10:45 休憩

10:45-11:40 セキュリティ　（座長：永藤直行 (立命館大)）

・セキュアVMにおけるIDEデバイスドライバの安全性検証(S)
  八木勲, 河合栄治, 関浩之 (奈良先端大), 品川高廣, 加藤和彦 (筑波大)
・情報流仕様からの言語組み込みアクセス制御文の自動挿入(P)
  高田喜朗 (高知工科大), 関浩之 (奈良先端大)
・仮想マシンに対する高いサービス可用性を実現するパケットフィルタリング(S)
  安積武志, 田所秀和, 光来健一, 千葉滋 (東工大)

11:40-11:45 クロージング

↑