Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics

    címtáras azonosítással

    vissza a tantárgylistához   nyomtatható verzió    

    Software Verification and Validation

    A tantárgy neve magyarul / Name of the subject in Hungarian: Szoftver verifikáció és validáció

    Last updated: 2018. április 27.

    Budapest University of Technology and Economics
    Faculty of Electrical Engineering and Informatics
    PhD course
    Course ID Semester Assessment Credit Tantárgyfélév
    VIMMD052   4/0/0/v 5 1/1
    3. Course coordinator and department Dr. Majzik István,
    Web page of the course
    4. Instructors Dr. István Majzik, Associate Professor, Department of Measurement and Information Systems (BME MIT)
    7. Objectives, learning outcomes and obtained knowledge 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.
    8. Synopsis
    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).
    9. Method of instruction Lectures.
    10. Assessment
    During the semester: Solution and presentation of an assigned homework. The successful completion of the homework is required for the signature and prerequisite of the exam.
    In the exam period: Oral exam.
    11. Recaps The homework assignment can be submitted during the repetition period.
    12. Consultations Consultations are offered by appointment.
    13. References, textbooks and resources
    Presentation slides available on the web page of the course.
    Gerard O'Regan: Concise Guide to Formal Methods: Theory, Fundamentals and Industry Applications. Springer, 2017.
    N. S. Godbole: Software Quality Assurance: Principles and Practices. 2nd edition, Alpha Science, 2016.
    B. Berard et. al.: Systems and Software Verification. Springer, 2007.
    G. G. Schulmeyer, G. R. MacKenzie: Verification and Validation of Modern Software-Intensive Systems. Prentice Hall, 2010.
    D. Peled: Software Reliability Methods. Springer, 2001.
    14. Required learning hours and assignment
    Lectures and classroom practice56
    Preparation for lectures14
    Preparation for mid-semester tests0
    Homework assignment25
    Study of selected written material15
    Preparation for exams40
    15. Syllabus prepared by
    Dr. István Majzik, Associate Professor, BME MIT