講演資料ダウンロード

形式手法活用ガイドと
辞書管理ツールを用いた
VDM適用事例
富士通九州ネットワークテクノロジーズ㈱
技術戦略室 開発技術部
井上 康生
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
富士通九州ネットワークテクノロジーズ㈱
富士通九州ネットワークテクノロジーズ㈱は、
ネットワーク関連のレガシーな技術ならびに、
多種多様な最先端技術を保有している開発会社です
事業内容
端末・ネットワークシステムのソフトウェア・ファームウェア・ハードウェアの
開発設計、システム構築業務、製造、販売、コンサルティング
キーデバイス（ＡＳＩＣ/ＦＰＧＡ）の開発設計
メディア信号処理機能の開発設計
所在地 本社
： 福岡県福岡市早良区
広島事業所 ： 広島県広島市中区
1
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
事業ドメイン
システム・ソリューション
ｻｰﾋﾞｽ・ﾏﾈｰｼﾞﾒﾝﾄ・ｿﾘｭｰｼｮﾝ
ﾈｯﾄﾜｰｸ・ﾏﾈｼﾞﾒﾝﾄ・ｿﾘｭｰｼｮﾝ
ネットワーク・テクノロジー
IP系ｼｽﾃﾑ開発
ﾌｫﾄﾆｯｸ系ｼｽﾃﾑ開発
・IPﾈｯﾄﾜｰｸ技術
・IPﾄﾗﾝｽﾎﾟｰﾄ技術
・有線系ｱｸｾｽ技術
・WDM技術
ﾈｯﾄﾜｰｸ制御技術
移動無線ﾈｯﾄﾜｰｸ技術
ﾓﾊﾞｲﾙ系ｼｽﾃﾑ開発
・WCDMA技術
・FMC技術
・ﾓﾊﾞｲﾙ系ｱｸｾｽ技術
キー・テクノロジー
ﾈｯﾄﾜｰｸｱﾌﾟﾘｹｰｼｮﾝ技術
ﾘｱﾙﾀｲﾑｼｽﾃﾑ技術
通信ﾌﾟﾛﾄｺﾙ技術
画像処理技術
ＡＳＩＣ/ＦＰＧＡ設計技術
アナログ設計技術
ﾃﾞｨｼﾞﾀﾙ信号処理技術
ＩＰ電話制御技術
実装／構造設計技術
etc
応用技術
応用分野
ﾃﾞｼﾞﾀﾙ家電
ﾜｲﾔﾚｽ通信
ｾｷｭﾘﾃｨ技術
ﾊﾞｲｵﾒﾄﾘｯｸｽ技術
2
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
形式手法への取り組み
２００９年度より、複数プロジェクトにて試行、適用
適用を通じ、形式手法の有効性を確認
検討工程、設計工程の品質向上
検証工程での仕様に起因する問題の削減
一方で、継続的適用や適用作業の標準化はこれからの課題
形式手法、VDMのスキル獲得が重要
適用事例の更なる拡大が必要
適用拡大のための施策
形式手法、VDMの有識者による支援、代行
社外、社内教育によるVDMスキル保有者の育成
有効性の認知／成功事例の増加・拡大
3
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
開発PJの概要、ＶＤＭの適用体制
対象：
工程：
入力：
狙い：
体制：
ネットワーク管理システム (規模 ： Ruby 3.2 Kstep)
検討（要求仕様、システム仕様、機能仕様）
構成図やシーケンス等の図を多用した顧客要求仕様書
設計工程の品質向上、および、ノウハウの獲得
開発チームとＶＤＭチームによる並行作業による適用
開発チーム
形式手法?
VDM++ ??
NW管理
システム
文書
シーケンス
VDM記述
構成図
あ
い
初の実適用
適用プロセス？
顧客要求仕様書
（イメージ）
ＶＤＭチーム
4
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
VDM適用における課題
課題１
開発への適用プロセスが不明
開発チームも
VDMチームも
実適用は初めて！
開発チームは
VDM++コードは
読めない！
課題２
チーム間のレビューがＶＤＭ++では出来ない
構成図は要求仕様？
シーケンス図は機能仕様？
課題３
図を多用した仕様書はＶＤＭ++の記述が困難
5
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
課題を解決する対策（課題１）

課題１
開発への適用プロセスが不明
開発チームも
VDMチームも
実適用は初めて！
開発チームは
VDMコードは
読めない！
課題２
形式手法適用手順（VDM++）編
チーム間のレビューがＶＤＭでは出来ない
構成図は要求仕様？
シーケンス図は機能仕様？
課題３
図を多用した仕様書はＶＤＭ記述が困難
6
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
形式手法適用手順（VDM++）編 の利用
中間成果物
クラス図
状態遷移図
制約条件一覧
ユースケース
記述票を利用
成果物
VDM要素一覧
成果物
辞書管理
ツールを利用
形式手法活用ガイドならびに参考資料 (IPA/SEC,2012/9)
図1 作業全体の流れ
[抜粋]
VDM++記述
課題を解決する対策（課題２）

課題１
開発への適用プロセスが不明
開発チームも
VDMチームも
実適用は初めて！
開発チームは
VDM++コードは
読めない！
課題２
チーム間のレビューがＶＤＭ++では出来ない
構成図は要求仕様？
シーケンス図は機能仕様？
課題３
ユースケース記述票
図を多用した仕様書はＶＤＭ記述が困難
辞書管理ツール
8
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
ユースケース記述票への期待
振る舞いの
記述により
レビューが
容易
制約条件が
明記され、
VDM++の記述
につながる
ユースケース記述票 （例）
9
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
ユースケース記述票の有効性（問題検出）
システムが繋いでくれる
ネットワーク上の経路
ﾕｰｽｹｰｽ名
ｲﾍﾞﾝﾄﾌﾛｰ
経路設定
ﾕｰｽｹｰｽ名
1. 経路設定要求を受信
2. 指定サーバ経路を決定
3. 経路上のVLANを設定
ＯＫならば3.1へ、
NGならば4へ
3.1 設定経路を
使用中経路情報
に追加
ｲﾍﾞﾝﾄﾌﾛｰ
経路変更（障害/輻輳）
1. 設定済の経路で経路
変更を抽出の場合、
2. 変更経路を抽出
3. 抽出経路のVLAN削除
4. 削除経路を
使用中経路情報から
削除
：
：
：
5.
4. 経路設定の結果を通知
： ：
5. 本ユースケースを終了
：
：
：
本ユースケースを終了
ユースケース記述票 （バグ検出例）
10
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
辞書管理ツールとは？
 九州大学）荒木研究室の大森洋一先生を中心に開発
 入力仕様書から、VDM++のコード作成までの作業を支援
①仕様書の語句を抽出
②抽出した語句を仕様書上でハイライト
③抽出語句と語句に対する形式記述等の属性を管理する辞書機能
④辞書からVDM++のコードを生成する自動生成
⑤VDMエディタ
 仕様書の語句とVDM++コードとをマッピングし、辞書として管理可能
日本語の仕様書
(自然言語)
仕様書 - VDM 連携ツール
（辞書管理ツール）
作成支援
フィードバック
VDM++コード
(ＶＤＭ開発環境)
自然言語仕様とVDM仕様
11
VDM++コードを
編集/検証
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
辞書管理ツール（辞書管理機能）
仕様書上の
重要な語句を抽出
⇒ハイライト
抽出語句は
辞書データ
で管理
仕様書上の
重要語句と
対応付け
用語辞書が作成される
辞書管理ツールの画面 1
12
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
辞書管理ツール（VDM出力機能）
仕様書の記述
VDM++コードを出力
対応付け
出力機能
VDM++の記述
辞書データをキーに
仕様書とVDM++コード
の対応付けが明確化
⇒ レビューが容易に
辞書の
詳細設定
辞書管理ツールの画面 2
13
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
課題を解決する対策（課題３）
開発チームも
VDMチームも
実適用は初めて！

課題１
開発への適用プロセスが不明
要求を階層化し仕様書を作成
開発チームは
VDMコードは
読めない！
課題２
チーム間のレビューがＶＤＭでは出来ない
構成図は要求仕様？
シーケンス図は機能仕様？
課題３
図を多用した仕様書はＶＤＭ++の記述が困難
14
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
適用の全体像
顧客要求仕様書
要求を階層化して整理
要求仕様検討
要求仕様書
システム仕様検討
詳細化
抽出
ｼｽﾃﾑ仕様書
機能仕様検討
詳細化
抽出
機能仕様書
抽出
ユースケース記述票
辞書管理ツール
適用
適用
ﾌｨｰﾄﾞﾊﾞｯｸ
要求仕様の
VDM++記述
ﾌｨｰﾄﾞﾊﾞｯｸ
適用
ﾌｨｰﾄﾞﾊﾞｯｸ
ｼｽﾃﾑ仕様の
VDM++記述
ﾌｨｰﾄﾞﾊﾞｯｸ
ﾌｨｰﾄﾞﾊﾞｯｸ
機能仕様の
VDM++記述
形式手法適用手順（VDM++）編
検出
検出
検出
曖昧性、不明確、不足・不備
15
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
適用による問題検出
UC：ユースケース記述票
要求仕様検討
検
出
問
題
数
機能仕様検討
仕様書
UC/VDM
仕様書
UC/VDM
仕様書
UC/VDM
小計
不明確
4
0
1
3
1
0
9
記載漏れ
2
1
0
5
0
2
10
冗長
0
0
0
0
0
0
0
矛盾
0
0
0
0
0
0
0
小計
6
1
1
8
1
2
19
2
108
3
312
4
416
生産量 Page| Line
工数
システム仕様検討
人H
16.8
32.5
106.1
開発データ(検出バグ数、生産量、工数）
実装、試験工程で、仕様に起因する問題検出
16
０件
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
適用の成果と課題
成果
形式手法適用手順（VDM++)編 が有効であることを確認
適用手順が未確定／スキル・経験が不充分な初心者向け
対象や条件に併せ、中間成果物の選択や内容追加等のカスタマイズ
ユースケース記述票 が有用であることを確認
VDM++で記述すべき内容が整理され、かつ明確になる
第三者レビューへの活用／複数UC記述票の比較により問題検出可能
辞書管理ツールが有用であることを確認
辞書管理機能 ： 仕様書上の重要語句が整理され、辞書として蓄積
モデル出力機能 ： 出力機能により仕様書とVDM++コードの対応付け
課題
辞書管理ツールで作成した辞書の再利用により適用を効率化
仕様記述のパターン化、や、VDM++記述を考慮した記述方法
設計工程以降 or 大規模開発 へ適用時の有効性検証
複数メンバ間における表現の統一、情報共有
17
Copyright 2013 Fujitsu Kyushu Network Technologies LIMITED
18
Copyright 2011 Fujitsu Kyushu Network Technologies LIMITED