The aim of the subject is a systematic 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 basis of formal verification techniques (model checking, equivalence checking, and proof of correctness) and the model based test case generation. The students will be familiar with the techniques that can be selected for checking the specification, design, and implementation of software applications, especially during model based development.

1. The role of verification and validation in the development process:Overview of the role of verification and validation (V&V) and their typical techniques in various development methodologies and standards. 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 architecture design: Review of the architecture design: systematic interface and fault-effect analysis techniques and architecture trade-off analysis. Model-based evaluation of functional and extra-functional properties (reliability, availability, performance, safety). 4. Verification of the detailed design: Design reviews. Formal verification of design models: model checking, equivalence checking, theorem proving. Specification of liveness and safety properties using temporal logics. Algorithms for checking temporal logic properties. Efficient handling of the state space of behavioral models by symbolic techniques, incremental model checking, and partial order reduction. Abstraction techniques (predicate abstraction, counterexample guided abstraction refinement). Checking the equivalence and refinement of design models.Model checking based verification of extra-functional (quality of service) properties.Formal verification of time-dependent behavior. 5. 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 program representation: 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. 6. Software testing: Unit testing by specification-based and structure-based techniques. Data flow based testing. Integration testing by incremental and scenario based techniques. Test quality metrics.Specific testing techniques: GUI testing, robustness testing, testing OO software. Source code based testing, symbolic execution.Model based test case generation using program graph based algorithms, model checkers, mutation based and evolutionary algorithms. Test conformance relations. Model based testing of context-aware autonomous behavior (case study). 7. Validation:Validation by review, testing and measurements.Verification and validation in case of changes and maintenance. Supporting techniques for re-verification (program slicing, incremental testing).