|
| STUDENTS
> Validation and Verification
|
Validation and Verification
Note:
Whilst every effort is made to keep the syllabus and assessment records correct
for this course, the precise details must be checked with the lecturer(s).
| Code: | GS03
(Also taught as: 4023)
|
| Year: | 4 |
| Prerequisites: | An understanding of the basics of programming and software engineering. |
| Term: | 2 |
| Taught By: | Graham Roberts (50%)
Alessio Lomuscio (50%)
|
| Aims: | The course will train students in the principles and techniques of validating and verifying complex software systems. The training will be at an intellectually demanding level and will cover not only the state-of-the practice in validation and verification, but also the most significant trends, problems and results in validation and verification research. |
| Learning Outcomes: | On completion of the course unit, the successful student should have a good knowledge and understanding of basic notions of correctness, consistency, faults and failures, testing and execution trace analysis. The successful student should also be able to understand the use of logic as a formal language for specification of systems, to understand the use of the main verification techniques used in symbolic model checking, to understand the architecture and be able to use a main tool (such as SMV) to verify simple systems. Further, successful students will be able to appreciate the limitations of the current tools and have insights in ongoing advanced research topics to overcome them.. |
Content:
| Basic concepts | Software engineering lifecycle context
Correctness
Consistency
Faults
Errors
Failures
Static and dynamic analysis |
| Introduction to static analysis | |
| Formal verification | Axiomatic specification
Hoare triples
Verification conditions
Proofs of correctness |
| Model checking | State-based program models
Finite-state models
Temporal logic specification
Symbolic model verification |
| Introduction to dynamic analysis | |
| Basic testing | The testing lifecycle
Control-flow program models
Data-flow program models
Coverage (whitebox) testing
Specification-based (blackbox) testing
Regression testing |
| Advanced testing | Operational profiles
Reliability testing
Performance and scalability testing
Regression testing
Fault injection
Mutation analysis
Testing concurrent and distributed programs
Testing component-based software |
| Execution analysis | Program instrumentation
Assertion checking
Trace analysis |
Method of Instruction:
Lectures, coursework, student-led seminars
Assessment:
The course has the following assessment components:
- Written Examination (2.5 hours, 85%)
- Coursework Section (2 pieces, 15%)
To pass this course, students must:
- Obtain at least 40% on the coursework component
- Obtain an average of at least 50% when the coursework and exam components of a course are weighted together
The examination rubric is:
Answer THREE questions.Resources:
Logics in Computer Science: Modelling and Reasoning about Systems. Huth and Ryan. Cambridge University Press. Second Edition, 2004
|
