[T4]形式手法 -効果的な活用に向けて ：詳細プログラム

1月19日（木）

13:45-14:00 オープニング
14:00-15:00 セッション1：形式仕様記述 （司会：横川智教）
  1. 形式仕様記述を用いた系統的なプロパティベーステストの活用
    馬場勇輔，荒木啓二郎（九州大学），日下部茂（長崎県立大学），大森洋一（九州大学）
  2. 要求辞書としての形式仕様詳細化手法の提案
    幡亮介，大森洋一，荒木啓二郎（九州大学），日下部茂（長崎県立大学）
15:00-15:15 休憩
15:15-16:15 セッション2：要求分析・検証(1) （司会：早水公二）
  1. STAMP/STPAを活用したVDM仕様記述の構築
    藤崎淳史，荒木啓二郎，大森洋一（九州大学）
  2. 時間ペトリネットを対象とした非有界モデル検査の高速化に関する検討
    井川直，横川智教，佐藤洋一郎，有本和民（岡山県立大学）
16:16-16:30 休憩
16:30-17:30 セッション3：要求分析・検証(2) （司会：早水公二）
  1. ペアワイズ法に基づいた検証項目の生成とモデル検査による組み込みシステムの検証に向けて
    渡辺誠人（日本大学），岡野浩三（信州大学），関澤俊弦（日本大学）
  2. 形式アシュアランスケースによる妥当性確認の形式化
    木下修司（神奈川大学）

1月20日（金）

10:00-11:00 セッション4：モデル化 （司会：横川智教）
  1. Kuromoji と構文解析による要求仕様書から状態遷移系への自動変換の試み
    田幸玄陽，小形真平，岡野浩三（信州大学），関澤俊弦（日本大学）
  2. 組込みソフトウェアを対象とした状態遷移表抽出手法とそのモデル検査への応用について
    山本椋太（名古屋大学）
11:00-11:30 全体ディスカッション
11:30-11:45 クロージング