ソフトウェア開発の形式工学手法
担当教員
授業の到達目標及びテーマ
学生に形式仕様記述技術の利点を理解してもらい、具体的なソフトウェアシステムの形式仕様作成のために必要な技術を身につけってもらうこと。
授業の概要と方法
形式工学手法は、実際のソフトウェア開発における最先端かつ厳密的な技術である。本講義では、形式工学手法の基本概念、システムの仕様作成技術、および適用手法などについて、多数の事例と事例研究を用いて講義する。特に、本講義は、SOFLという代表的な形式工学手法を中心として紹介し、構造化設計、オブジェクト指向設計、および形式記述技術を統合したアプローチをソフトウェア開発に適用することを説明する。本講義を勉強する学生らは、システム形式仕様記述技術、設計、および形式仕様によって実装する手法など技術を勉強できる。また、形式工学手法は、ソフトウェア開発の生産性と品質の改善にどのように働くできるかも説明する。 Formal engineering methods are the most advanced and rigorous technology for industrial software development. The concepts involved in formal engineering methods and their applications to functional specification construction of software systems are explained through many examples and small case studies. In particular, this course focuses on the introduction to the SOFL method that integrates the structured method, object-oriented method, and formal methods for software development. Students attending this course are expected to learn many effective techniques for writing requirements specifications, carrying out systems design, and transforming specifications into programs. Furthermore, through this course students are also expected to understand how formal methods can be effectively integrated into the entire software development process to enhance the productivity and reliability of software systems.
授業計画
| 回 | テーマ | 内容 |
|---|---|---|
| 1 | はじめ1(Introduction1) | ソフトウェア開発の問題点、この問題点を解決するために提案された形式手法を紹介します。 |
| 2 | はじめ2(Introduction 2) | 形式手法が適用される 時の困難、この困難を克服するために提案された形式工学手法などを論議します。 |
| 3 | 命題論理と述語論理(Propositional and Predicate logics) | 命題論理と述語論理の基本概念を紹介します。更に、それらの概念の形式仕様記述言語にの表現仕方も説明します。 |
| 4 | プロセス仕様1(Process specification1) | SOFL形式仕様記述言語、仕様とプログラムの関係、プロセスの構文と意味を説明します。 |
| 5 | プロセス仕様2(Process Specification2) | 事前条件と事後条件を紹介する上で、形式仕様に基づきどのようにプログラムを作成し、そのプログラムをテストすることを説明します。 |
| 6 | 複合式と関数の形式仕様(formal function specification) | 複合式、関数の陽定義と陰定義の仕組を紹介します。 |
| 7 | 形式仕様の作成技術(Techniques for writing formal specifications ) | 条件データフロー(CDFD)とモジュールの対応関係、モジュールの各部分の内容を紹介します。 |
| 8 | 基本型(Basic types) | 基本型の概念、必要な操作、およびこの型の形式仕様にの適用事例分析を論議します。 |
| 9 | 集合型(Set types) | 集合型の概念、必要な操作、およびこの型の形式仕様にの適用事例分析を論議します。 |
| 10 | 列型と文字列型(Sequence and string types ) | 列型と文字列型の概念、必要な操作、およびこれらの型の形式仕様にの適用事例分析を論議します。 |
| 11 | 複合型(Composite) | 複合型の概念、必要な操作、およびこの型の形式仕様にの適用事例分析を論議します。 |
| 12 | 写像型(Map types)形式設計仕様(Formal specification in design ) | 写像型の概念、必要な操作、およびこの型の形式仕様にの適用事例分析を論議します。 |
| 13 | 合併型(union type) | 合併型の概念、必要な操作、およびこの型の形式仕様にの適用事例分析を論議します。 |
| 14 | 形式仕様記述の三段回アプローチ(Three-step formal specification approach) | SOFL三段階形式仕様記述アプローチを紹介します。非形式仕様段階、半形式仕様段階、および形式仕様段階の具体的なタスクおよび各段階の仕様がソフトウェア開発の上流段階にどのような役割を発揮するかを論議します。 |
| 15 | 綜合復習 | 勉強した形式手法、形式工学手法、およびソフトウェア工学との関係、形式仕様の作成技術などを総合復習し、簡単な事例研究を学生に行ってもらいます。 |
授業外に行うべき学習活動
宿題
テキスト
“Formal Engineering for Industrial Software Development using the SOFL Method”, by Shaoying Liu, Springer-Verlag, March, 2004.
参考書
1.“Systematic Software Development using VDM”, by Cliff B. Jones, Prentice-Hall, 1990. 2.“Software Engineering”, by Ian Sommerville, Addision-Wesley, Sixth Edition, 2001.
成績評価基準
試験(Examination)80% 出席(Presence)20%
情報機器使用
デジタルプロジェクタ
前年度の授業改善アンケートからの気づき
もっと事例を用いて説明すること。
その他
この課程は、最強なSEになって、大手企業でSEとして活躍したい又は本分野の研究者になりたい学生に設定した授業です。コンピュータ科学の学生は、必ず勉強することを勧めます。