Software Verification and Validation
年度
- 2013 年度版
Instructor
Goal and Theme
Software specification, verification and validation
授業の到達目標
The students are expected to learn basic techniques for writing formal specifications, verifying the correctness of simple programs using Hoare logic, understand the basic principle of model checking, and use specification-based inspection and testing technqiues.
Abstract
This class introduces an integrated technology for software quality assurance. The technology includes formal specification techniques based on the SOFL specification language, and four
different verification and validation techniques that are (1) formal verification based on Hoare logic, (2) model checking, (3) specification-based insepction, and (4) specification-based testing. The formal specification technique is usually applied in the early phase of software development to prevent and remove requirements and design-related errors, while the four verification and validation techniques target on program errors. The Hoare logic-based formal verification are more theoretical, while the specification-based inspection and testing are more practical. By introducing the theoretical techniques, students are expected to learn basic concepts such as the partial and total correctness of programs, program models, state, state transition, and formal proof. By introducing the practical techniques, students are expected to learn rigorous but practically useful verification and validation technqiues, such as specification-based inspection, functional scenario-based testing, and the relation between specification and program.
The class is taught by means of lectures, class exercises, and homework. Sometimes, students are also required to present some part of the teaching material.
Schedule
| 回 | テーマ | 内容 |
|---|---|---|
| 1 | Formal verification of program correctness | Partial correctness, total correctness, program state, assertions, and Hoare logic. |
| 2 | Axioms for assignment and conditional statements | Axioms for assignments, examples, axioms for conditional statements, and examples. |
| 3 | Axioms for iterations | Invariant of while loop statement, axiom for while loop, examples, and how can formal proof be used to help find bugs in programs. |
| 4 | Requirements and formal specification | formalization for requirements and design quality. |
| 5 | Logic and Specification | Propositional logic, Predicate logic and Process specification |
| 6 | Basic types and Set types | Numeric types, enumeration types, relation, set type definition, constructors, and operators |
| 7 | Sequence and string types | Sequence type definition, constructors, and operators. |
| 8 | Composite and product types | Composite type definition, constructor, operators, product type definition, constructor, and operators. |
| 9 | Map types | Map type definition, constructors, and operators. |
| 10 | Three steps for formal specifications | Informal specification, semi-formal specification, and formal specification. |
| 11 | Introduction to model checking | The problem to be solved by model checking, the principle of model checking. |
| 12 | CTL and finite state machine | CTL, state transition, finite state machine. |
| 13 | Specification-based inspection principle | What is inspection? the principle of specification-based inspection. |
| 14 | Specification-based inspection strategy and process | Derivation of functional scenarios, derivation of program pathes, linking scenarios to paths, checking paths, and producing an inspection report. |
| 15 | Specification-based testing | Principle, strategy, process, and examples. |
授業外に行うべき学習活動 (準備学習等)
Preview the contents of each class, complete the assigned exercises, and review the contents taught in the class. If possible, read related materials.
Materials
“Formal Engineering for Industrial Software Development”, Shaoying Liu, Springer-Verlag, 2004, ISBN 3-540-20602-7.
References
(1) C.A.R. Hoare and C. B. Jones, ``Essays in Computing Science'', Prentice Hall, 1989
(2) E. M. Clarke, O. Grumberg, and D. A. Peled, ``Model Checking'' the MIT Press, 1999.
Evaluation Method
Report (40%), presentation (20%), and homework (40%)
情報機器使用
PC, paper, and pen.
学生による授業改善アンケートからの気づき
None
Remarks
The knowledge offered in this course provides a foundation for understanding and supporting the development of correct software systems.