KA238201 ソフトウェア工学II

広島大学シラバス

English

年度 2025年度開講部局情報科学部

講義コード KA238201 科目区分専門教育科目

授業科目名ソフトウェア工学II

授業科目名
（フリガナ）ソフトウェアコウガク２

英文授業科目名 Software Engineering II

担当教員名劉　少英

担当教員名
(フリガナ) リュウ　ショウエイ

開講キャンパス東広島開設期 3年次生後期集中

曜日・時限・講義室 (集) 集中：オンライン

授業の方法講義授業の方法
【詳細情報】オンライン（同時双方向型）

集中講義

単位 2.0 週時間　使用言語 J : 日本語

学習の段階 4 : 上級レベル

学問分野（分野） 25 : 理工学

学問分野（分科） 02 : 情報科学

対象学生 3年生

授業のキーワードソフトウェア工学、形式仕様、Hoare論理、ソフトウェアテスト、品質保証

教職専門科目　教科専門科目　

プログラムの中での
この授業科目の位置づけ
（学部生対象科目のみ）形式仕様、Hoare論理、およびソフトウェアテストの役割と具体的な技術を理解し、それらを実践的に体験することで、実際のソフトウェアシステムの品質保証に役立つ知識を習得することを到達目標として設定しています。
到達度評価
の評価項目
（学部生対象科目のみ）計算機科学プログラム
（総合的な力）
・D2. 多様化，複雑化した情報社会における分野横断的な課題に対して，豊富な最先端情報技術に基づいて，最適なシステムソリューションを導く能力．

データ科学プログラム
（能力・技能）
・A. 情報基盤の開発技術，情報処理技術，データを分析して新しい付加価値を生む技術．

知能科学プログラム
（総合的な力）
・D3. 複合的に絡み合う社会的ニーズや課題を俯瞰的に捉え，知能科学の幅広い知識に基づいた多角的視野と分析能力で課題を解決する能力．

授業の目標・概要等ソフトウェア工学Iの講義で紹介された基本的なソフトウェア工学の概念を基盤に、ソフトウェア品質保証の向上を目的とした先進的な手法と技術について紹介します。具体的には、以下の三つの理論と技術に焦点を当てて講義を進めます。第一に、実用的な形式仕様記述技術を紹介し、クラス練習を通じて学生が実際に仕様記述を体験できるようにします。また、形式仕様記述技術を活用して要求に関連するエラーを未然に防ぐ方法についても議論します。第二に、プログラムの正しさを形式的に証明するHoare論理を取り上げ、具体的な事例を通じて、実装されたプログラムが形式仕様を満たすかどうかを形式的に検証する技術を講義します。第三に、プログラムの振る舞い評価とバグ検出に有効なソフトウェアテストの手法と技術を紹介し、形式検証と比較してその利点と課題について議論します。

授業計画第1回：ソフトウェア品質保証についての基本概念と技術を紹介する。ソフトウェア品質保証とは何か、ソフトウェア工学との関係、品質保証の段階、および代表的な技術を具体的な内容として講義する。
第2回：SOFL仕様記述言語を基に、形式仕様記述仕組みと技術を紹介する。特に、事前条件と事後条件の仕様記述技術に集中して講義する。
第3回：機能シナリオフォームという実用性が高い形式仕様の仕組みを紹介し、その記述技術について説明する。
第4回：複雑な機能を表現する形式仕様記述するために必要なデータ型を紹介する。初回は基本型と集合かたを講義する。
第5回：列型、複合型、および積集合型を紹介し、事例を用いてそれらの使い方を説明する。
第6回：写像型と和集合型を紹介し、事例を使ってそれらの使用し方を解釈する。
第7回：形式仕様記述の「三段階」技術を紹介しながら、要求に関わるエラーを防止する技術も論議する。
第8回：Hoare論理の基本概念を紹介し、プログラムの正確性という重要な概念の定義を説明する。その上で、代入文の正確性を検証するために必要な公理を紹介しながら、クラス練習もすることにより、その公理の使い方を理解してもらう。
第9回：順序構造および条件構造の正確性を検証するに使われる公理を紹介しながら、クラス練習により、それらの公理の適用し方を体験してもらう。
第10回：反復構造の正確性を検証するために必要な公理を、分かりやすい事例を用いて紹介する。
第11回：ソフトウェアテストについての基本概念と手法を紹介する。特に、ハイトボックステスト、ブラックボックステスト、およびグレーボックステストに関する基本概念を説明、様々なテストカバレッジを紹介する。
第12回：形式仕様についての自動テスト手法と技術を紹介する。特に、テストデータの自動生成手法とアルゴリズム、テストオラクルの自動生成と適用方法に集中して講義する。
第13回：簡単化されたATMソフトウェアを事例として使い、形式仕様記述および仕様によってプログラムの実装を行うsmall project 1を演習する。
第14回：簡単化されたATMソフトウェアを事例として使い、テストデータの生成およびテストオラクルの生成を行うsmall project 2を演習する。
第15回：簡単化されたATMソフトウェアを事例として使い、生成されたテストデータおよびテストオラクルを用いて、実装されたプログラムのテストを行い、バグを発見して、コードの間違いを修正するsmall project 3を演習する。

紹介する技術の基本概念、原理、および実践的な技術を、分かりやすい事例を交えながら講義し、クラス練習や討議を通じて学生とのインタラクションを強化します。これにより、講義内容の理解度を深めます。また、学生が技術を実際に体験できるように、復習、予習、宿題への指導を行い、その経験についてクラスで議論する時間を設けます。

教科書・参考書等講義資料（PPT）

授業で使用する
メディア・機器等配付資料, Microsoft Teams

【詳細情報】

授業で取り入れる
学習手法

予習・復習への
アドバイス講義内容を配布資料に従って復習することが望ましい。

履修上の注意
受講条件等

成績評価の基準等レポートによる評価を予定してる

実務経験

実務経験の概要と
それに基づく授業内容

メッセージ

その他参考資料：
1． Shaoying Liu, "Formal Engineering for Industrial Software Development using the SOFL Method", Springer-Verlag, March 2004, 428 pages, ISBN 3-540-20602-7.
2． Shaoying Liu, “Agile-SOFL: Agile Formal Engineering Method”, Springer-Nature, June 2024, ISBN 978-981-97-2285-3.

すべての授業科目において，授業改善アンケートを実施していますので，回答に協力してください。
回答に対しては教員からコメントを入力しており，今後の改善につなげていきます。

年度	2025年度	開講部局	情報科学部
講義コード	KA238201	科目区分	専門教育科目
授業科目名	ソフトウェア工学II
授業科目名（フリガナ）	ソフトウェアコウガク２
英文授業科目名	Software Engineering II
担当教員名	劉　少英
担当教員名 (フリガナ)	リュウ　ショウエイ
開講キャンパス	東広島	開設期	3年次生後期集中
曜日・時限・講義室	(集) 集中：オンライン
授業の方法	講義	授業の方法【詳細情報】	オンライン（同時双方向型）
集中講義
単位	2.0	週時間		使用言語	J : 日本語
学習の段階	4 : 上級レベル
学問分野（分野）	25 : 理工学
学問分野（分科）	02 : 情報科学
対象学生	3年生
授業のキーワード	ソフトウェア工学、形式仕様、Hoare論理、ソフトウェアテスト、品質保証
教職専門科目		教科専門科目
プログラムの中でのこの授業科目の位置づけ（学部生対象科目のみ）	形式仕様、Hoare論理、およびソフトウェアテストの役割と具体的な技術を理解し、それらを実践的に体験することで、実際のソフトウェアシステムの品質保証に役立つ知識を習得することを到達目標として設定しています。
到達度評価の評価項目（学部生対象科目のみ）	計算機科学プログラム（総合的な力）・D2. 多様化，複雑化した情報社会における分野横断的な課題に対して，豊富な最先端情報技術に基づいて，最適なシステムソリューションを導く能力．データ科学プログラム（能力・技能）・A. 情報基盤の開発技術，情報処理技術，データを分析して新しい付加価値を生む技術．知能科学プログラム（総合的な力）・D3. 複合的に絡み合う社会的ニーズや課題を俯瞰的に捉え，知能科学の幅広い知識に基づいた多角的視野と分析能力で課題を解決する能力．
授業の目標・概要等	ソフトウェア工学Iの講義で紹介された基本的なソフトウェア工学の概念を基盤に、ソフトウェア品質保証の向上を目的とした先進的な手法と技術について紹介します。具体的には、以下の三つの理論と技術に焦点を当てて講義を進めます。第一に、実用的な形式仕様記述技術を紹介し、クラス練習を通じて学生が実際に仕様記述を体験できるようにします。また、形式仕様記述技術を活用して要求に関連するエラーを未然に防ぐ方法についても議論します。第二に、プログラムの正しさを形式的に証明するHoare論理を取り上げ、具体的な事例を通じて、実装されたプログラムが形式仕様を満たすかどうかを形式的に検証する技術を講義します。第三に、プログラムの振る舞い評価とバグ検出に有効なソフトウェアテストの手法と技術を紹介し、形式検証と比較してその利点と課題について議論します。
授業計画	第1回：ソフトウェア品質保証についての基本概念と技術を紹介する。ソフトウェア品質保証とは何か、ソフトウェア工学との関係、品質保証の段階、および代表的な技術を具体的な内容として講義する。第2回：SOFL仕様記述言語を基に、形式仕様記述仕組みと技術を紹介する。特に、事前条件と事後条件の仕様記述技術に集中して講義する。第3回：機能シナリオフォームという実用性が高い形式仕様の仕組みを紹介し、その記述技術について説明する。第4回：複雑な機能を表現する形式仕様記述するために必要なデータ型を紹介する。初回は基本型と集合かたを講義する。第5回：列型、複合型、および積集合型を紹介し、事例を用いてそれらの使い方を説明する。第6回：写像型と和集合型を紹介し、事例を使ってそれらの使用し方を解釈する。第7回：形式仕様記述の「三段階」技術を紹介しながら、要求に関わるエラーを防止する技術も論議する。第8回：Hoare論理の基本概念を紹介し、プログラムの正確性という重要な概念の定義を説明する。その上で、代入文の正確性を検証するために必要な公理を紹介しながら、クラス練習もすることにより、その公理の使い方を理解してもらう。第9回：順序構造および条件構造の正確性を検証するに使われる公理を紹介しながら、クラス練習により、それらの公理の適用し方を体験してもらう。第10回：反復構造の正確性を検証するために必要な公理を、分かりやすい事例を用いて紹介する。第11回：ソフトウェアテストについての基本概念と手法を紹介する。特に、ハイトボックステスト、ブラックボックステスト、およびグレーボックステストに関する基本概念を説明、様々なテストカバレッジを紹介する。第12回：形式仕様についての自動テスト手法と技術を紹介する。特に、テストデータの自動生成手法とアルゴリズム、テストオラクルの自動生成と適用方法に集中して講義する。第13回：簡単化されたATMソフトウェアを事例として使い、形式仕様記述および仕様によってプログラムの実装を行うsmall project 1を演習する。第14回：簡単化されたATMソフトウェアを事例として使い、テストデータの生成およびテストオラクルの生成を行うsmall project 2を演習する。第15回：簡単化されたATMソフトウェアを事例として使い、生成されたテストデータおよびテストオラクルを用いて、実装されたプログラムのテストを行い、バグを発見して、コードの間違いを修正するsmall project 3を演習する。紹介する技術の基本概念、原理、および実践的な技術を、分かりやすい事例を交えながら講義し、クラス練習や討議を通じて学生とのインタラクションを強化します。これにより、講義内容の理解度を深めます。また、学生が技術を実際に体験できるように、復習、予習、宿題への指導を行い、その経験についてクラスで議論する時間を設けます。
教科書・参考書等	講義資料（PPT）
授業で使用するメディア・機器等	配付資料, Microsoft Teams
【詳細情報】
授業で取り入れる学習手法
予習・復習へのアドバイス	講義内容を配布資料に従って復習することが望ましい。
履修上の注意受講条件等
成績評価の基準等	レポートによる評価を予定してる
実務経験
実務経験の概要とそれに基づく授業内容
メッセージ
その他	参考資料： 1． Shaoying Liu, "Formal Engineering for Industrial Software Development using the SOFL Method", Springer-Verlag, March 2004, 428 pages, ISBN 3-540-20602-7. 2． Shaoying Liu, “Agile-SOFL: Agile Formal Engineering Method”, Springer-Nature, June 2024, ISBN 978-981-97-2285-3.
すべての授業科目において，授業改善アンケートを実施していますので，回答に協力してください。回答に対しては教員からコメントを入力しており，今後の改善につなげていきます。

シラバスTOPへ