Advanced Software Engineering
- 2012 年度版 (2013年度版準備中)
Instructor
Goal and Theme
Formal engineering methods for software development
Abstract
This class introduces the latest formal engineering method for software development. After introducing the basic concepts, the lectures will concentrate on the discussion of the techniques for writing formal software specifications. In particular, it focuses on the Structured Object-Oriented Formal Language (SOFL) and its associated method. Students are given a chance to use SOFL to develop a library system on a small project and to learn how programs implemented based on the specifications can be inspected and testing.
Schedule
| 回 | テーマ | 内容 |
|---|---|---|
| 1 | Introduction | Software engineering problems, formal methods, and formal engineering methods are briefly introduced. |
| 2 | Propositional and Predicate logics | The basic concepts such as proposition and predicate are introduced, and the syntax and semantics of the logics are explained. |
| 3 | Process specification | Process is the most important component in a SOFL specification. In this part, the structure of a process specification is explained. |
| 4 | Techniques for writing specifications | How to write a process specification using pre- and post-conditions is explained. |
| 5 | Basic types and Set types | All of the basic types are introduced, and necessary operators are explained, and an example is used to demonstrate how the basic types can be used in a process specification. |
| 6 | Sequence and string types | The concepts of sequence, sequence type and string type are explained, and all of the useful operators are introduced. |
| 7 | Composite and product types | The concepts of composite type and product type are explained, and their operators are introduced. Several examples are used to show how the operators can be used in process specifications. |
| 8 | Map types and union types | The concepts of map type and union type are explained, and their operators are introduced. Several examples are used to show how the operators can be used in process specifications. |
| 9 | Formal specification in design | How formal specification technique is used to design a software. The idea of using condition data flow diagram (CDFD) to design the architecture of the system and to use pre- and post-conditions to specify the semantics of the processed involved. |
| 10 | Three steps for formal specifications | SOFL three-step formal specification approach is explained and an example is used to show how it works. |
| 11 | A case study | A case study on the use of the SOFL three-step approach is explained. |
| 12 | Specification-based inspection | If time allows, formal specification-based program inspection technique is explained. |
| 13 | Specification-based testing1 | If time allows, formal specification-bsed testing techniques are explained. |
| 14 | Specification-based testing2 | If time allows, formal specification-bsed testing techniques are explained. |
| 15 | Summary and review | All of the contents are summarized and reviewed. |
授業外に行うべき学習活動
read the SOFL book to learn more about the SOFL fomral engineering methods. The textbook can be bought from the university shop.
Materials
“Formal Engineering for Industrial Software Development”, Shaoying Liu, Springer-Verlag, 2004, ISBN 3-540-20602-7.
References
“Programming form Specifications”, Carroll Morgan, Printice-Hall, 1998.
Evaluation Method
Report (50%) and examination (50%)
情報機器使用
PC
前年度の授業改善アンケートからの気づき
None
Remarks
The knowledge offered in this course provides a foundation for understanding and supporting the development of correct software systems.