形式仕様記述（実践編）
平成２４年度シラバス
２０１２年４月１日
国立情報学研究所
トップエスイープロジェクト
代表者 本位田 真一
形式仕様記述（実践編）
石川 冬樹，栗田 太郎
本講義では，仕様を主として，開発上流における成果物（モデル・文書）の品質を高めるとともに，それらを開発プロセスにおいて効果的・効率的に活用するための考え方について学びます．本講義では，仕様書の品質維持・向上における課題を，自然言語の曖昧さや，記述漏れや記述間の矛盾・競合，保守や派生開発におけるトレーサビリティなど，様々な観点から議論します．その上で，特に形式手法・形式仕様記述の利点と限界を明らかにすることによって，自然言語や図表なども含めた記述方式による課題解決，分析・検証方式による課題解決，それらの適用方法や運用の工夫による課題解決などを，総合的に議論します．
本講義では上記の議論を通して，形式手法・形式仕様記述における利点・限界，適用の際に必要となる検討事項，オブジェクト指向など他の技術や開発プロセス全体との関連を理解することを目指します．これにより，形式手法・形式仕様記述（その裏にある原則・考え方）を，自身の課題と関連づけることができるようになることを目指します．
各自が持つ問題意識の洗い出しや，それに対する解決策の議論などを通し，問題点とその解決策の対応関係に関する本質的な理解を促す点．形式手法・形式仕様記述について，それ自身（言語やツールなど）を利用するための知識・スキルを，どう実際に開発の現場の課題解決に活用するかを主な課題とし，他技術との関連も含めて総合的に議論する点．
仕様をはじめとした開発上流の成果物における品質（特に信頼性）を確保し，それを軸として開発プロセスを安定化・効率化することは非常に重要です．しかし品質を達成する際の課題，そのための施策は多種多様であり，問題を系統的に整理し自身の状況に対して的確な施策を選択・定義することは簡単ではありません．関連して，形式手法・形式仕様記述が注目されていますが，その利点・欠点を把握して，適切な活用方法を定めることも簡単ではありません．本講義ではこれらの難しさと各自が向き合うために必要な素養を身につけるため，仕様などにおける問題や対応する施策に関する整理，議論を行います．
本講義では、仕様をはじめとした開発上流の成果物に関する課題と，形式手法・形式仕様記述を中心として，既存の代表的なアプローチとの対応関係の理解を身につけます．まこれにより，それらのアプローチを実際に活用する是非の判断や，活用方法の決定を行うための基本的な理解・素養を身につけます．
本講義の受講生は，下記の基礎知識を有していることが望まれます．
Ÿ ソフトウェア工学に関する基礎知識．特に，開発プロセス，上流工程やその成果物（要求仕様や機能仕様，設計など）の役割，オブジェクト指向．
Ÿ 形式仕様記述に関する基礎知識．すなわち，集合論と命題論理・一階述語論理を裏付けとした厳密なモデル化・記述，分析・検証の考え方．「形式仕様記述（基礎・VDM編）」にて学ぶ．
また下記のような経験，問題意識・疑問を持つ受講生を特に歓迎します．
Ÿ 仕様の品質（仕様に起因する手戻り・バグ）や，その品質を維持・向上するための記述と分析・検証の方法について，業務での経験や問題意識・疑問を持つ．
Ÿ 形式仕様記述（や形式手法全般）の活用是非，活用方法について，業務での経験や問題意識・疑問を持つ．
（実際の講義時間の配置などにより多少変更することがあります）
第１〜２回 イントロダクション・仕様記述に関する課題議論
Ÿ イントロダクション
Ÿ グループ議論
第３〜４回 事例議論
Ÿ 様々な事例の概観
Ÿ 具体的な事例に関する議論
第５〜７回 課題に対する施策の議論
Ÿ グループ議論・発表
Ÿ まとめ
本講義を受講することにより，形式仕様記述の手法・ツールをはじめとした様々な課題解決の手段の利点・限界を理解し，各開発プロジェクトの特性に合わせて必要な検討を行い適用することにより，開発の信頼性・効率を高めることができます．
本講義では特にツールを利用しません．
下記に関するグループ議論を行います．
Ÿ 仕様など開発上流の成果物における課題
Ÿ それらの課題と様々な施策との対応関係，個々の施策の利点・限界や活用に必要な検討事項
議論への参加とレポート課題を通して評価します．
なし
Ÿ フォーマルメソッド導入ガイダンス
三菱総合研究所， http://formal.mri.co.jp/ ，2011
Ÿ 「形式手法適用調査」報告書
情報処理推進機構 ソフトウェア・エンジニアリング・センター（IPA-SEC），
http://sec.ipa.go.jp/reports/20100729.html
，2010
Ÿ 形式手法活用ガイド，
Dependable Software Forum， http://www.nttdata.co.jp/dsf/
，2011
特定の形式手法・ツールの活用，応用事例，ソフトウェア工学の原則などについて，その他の書籍，報告書，論文も適宜引用します．