Software Verification and Validation

Tárgyfelelős: 
Majzik István
Oktatók: 
Majzik István

Actual information

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.

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:

  1. 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.
  2. 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.
  3. 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 October 31, 2020.
  • The presentations will be scheduled in the last two weeks of the semester (in December 2020).
  • 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 answered, the other can be skipped (the pairs of exam topics are published in advance).

Presentations and abstracts submitted during the previous years can be checked here.

Detailed information regarding the online exams in the first semester of 2020/21

  • Exam dates are December 17., January 7., 14., and 21. Each exam starts at 14:15 in the afternoon.
  • These dates of the exams will be published in the Neptun system (when the exam registration period will start). You have to register for your selected exam in Neptun.
  • The exam is oral. In the time of the exam, you have to login to Teams (i.e., be online available) and wait until the lecturer will call you when your slot in the exam will start.
  • Since there was no chance to meet personally during the semester, you will be asked to present your identity card (with your photo) in the camera.
  • At the beginning of your exam, the lecturer will randomly select one pair of topics from the complete list of topics and you have to present (explain) these topics.
  • If you had an oral presentation of your homework, then only one of the two topics shall be explained, the other can be skipped.
  • As it is an oral exam, the goal is to explain the concepts and the basic ideas related to the selected topic(s); e.g., what are the properties that are verified using a given technique; what is represented (and how) by the given formalism; what is the basic approach of the algorithm that is applied for verification; what are the advantages or disadvantages. It is not necessary to present formula, detailed proofs etc.