Software Verification and Validation
Current information in 2021 (fall semester)
- From 2021, course materials will be posted to the Faculty's Moodle system.
Overview
Objectives
The aim of the course is to provide an overview of the verification and validation techniques that are typically used in software development. The lectures discuss the classic verification and validation methods (review, analysis and testing) as well as the mathematical basics of formal verification techniques (model checking, equivalence checking, and proof of correctness) and model based test case generation. The students will be familiar with the techniques that can be selected for the systematic checking of specification, design, and implementation of software applications, especially during model based development.
Synopsis
1. The role of verification and validation in the development process.
- Development methodologies and standards. Overview of the role of verification and validation (V&V) and their typical techniques. The role of formal verification.
2. Verification of the specification
- Overview and categorization of informal, semi-formal and formal specification languages.
- Aspects of checking the specification (completeness, consistency, testability, feasibility).
3. Verification of the design
- Verification of the architecture design: Review of the architecture (architecture trade-off analysis) and model-based evaluation of functional and extra-functional properties (reliability, availability, performance, safety).
- Verification of detailed design: Design reviews. Formal verification of design models: Model checking, equivalence checking, theorem proving. Specification of liveness and safety properties using temporal logics (LTL and CTL). Algorithms for checking temporal logic properties. Efficient handling of the state space of behavioral models: Symbolic techniques (ROBDD), incremental model checking, partial order reduction. Abstraction techniques (predicate abstraction, counterexample guided abstraction refinement). Equivalence and refinement checking of design models.
- Model checking based verification of extra-functional (quality of service) properties.
- Formal verification of time-dependent behavior.
4. Verification of the implementation
- Checking of the source code: static analysis, source code metrics, abstract interpretation.
- Proof of correctness based on the source code or detailed design: Mathematical techniques (computational and structural induction). Formalization of program correctness and termination. Proof of correctness in simple deterministic programs and programs written in structural languages. Properties and limitations of theorem proving tools.
- Software testing: Unit testing by specification-based and structure-based techniques. Integration testing by incremental (top-down and bottom-up) techniques. Data flow based testing. Test quality metrics.
- Specific testing techniques: GUI testing, robustness testing, testing OO software. Source code based testing, symbolic execution.
- Model based test case generation. Model based testing of context-aware autonomous behavior (example).
5. Validation
- Validation by review, testing, and measurements.
- Verification and validation in case of changes and maintenance. Supporting techniques (slicing, incremental testing).
Assessment
At the end of the semester: The assessment consists of an oral exam. It is based on a randomly assigned pair of topics, that shall be explained.
During the semester: The prerequisite of the exam is the presentation of a case study in the field of software verification and validation. The case study can be selected and presented in one of the following ways:
-
Oral presentation of a case study (and submission of the slide set in PDF format) that is based on a (previous) work of the student. Review, analysis, testing, or formal verification activity can be presented that includes a novel approach, an interesting technique, or a useful tool. The presentation should introduce the context and objectives, the selected V&V approach and tool, the outcome and the lessons learnt. The length of the presentation is 20 minutes.
-
Oral presentation of a case study (and submission of the slide set in PDF format) that is based on a selected publication (conference or journal paper, for example from the journal on Software Tools for Technology Transfer, the conference series on Formal Methods for Industrial Critical Systems etc.). The selected publication should describe a generally useful technique or tool (very specific approaches should be avoided). The presentation should show the context and objectives, the selected V&V approach and tool, the outcome and the lessons learnt. The length of the presentation is 20 minutes.
- Submission of an abstract in writing (4-5 pages) that summarizes a case study based on the (previous) work of the student or based on a selected publication (conference or journal paper). The abstract should show the context and objectives, the selected V&V approach and tool, the outcome and the lessons learnt.
It is important that the presentation of a modeling, design or implementation activity is not sufficient, as the focus shall be a verification or validation activity using a technique or tool that is interesting and generally usable.
In case of selecting option 1 or 2:
- Please negotiate the topic of the presentation with the instructor in email (at <majzik@mit.bme.hu>) not later than end of October.
- The presentations will be scheduled in the last two weeks of the semester.
- The length of the presentation is maximum 20 minutes.
- The successful presentation allows the student to utilize the following option during the oral exam: only one of the two exam topics shall be explained, the other can be skipped.
Presentations and abstracts submitted during the previous years can be checked here.
