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

    Belépés
    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: 2017. május 31.

    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, Méréstechnika és Információs Rendszerek Tanszék
    Web page of the course http://www.mit.bme.hu/oktatas/targyak/vimmd052
    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 course is the overview of the (formal) property specification and design languages, the verification methods and the validation techniques used in software development. The lectures discuss the mathematical basics of the discussed formalisms and methods (formal languages and semantics, verification algorithms), as well as the classic and model-based testing methods.
    The students will be familiar with techniques and tools that allow the precise description of software designs and the verification of their required properties.

    8. Synopsis
    1. Overview: The role of verification and validation in the development process. Software quality assurance. Design methodology and development standards. The role of formal methods.
    2. Formal specification: The role of formal specification languages and their classification. Model-oriented languages, process description languages, logic and hybrid languages. Object-oriented specification languages. 
    Formal specification of dependability and performance properties (continuous stochastic logics).
    3. Verification: The role of the formal semantics of the specification and design languages. Typical verification techniques: model checking, equivalence checking, theorem proving. Model checking for temporal logic specifications. The handling of large state spaces by symbolic techniques. Abstraction and state space reduction techniques.
    Equivalence checking: Strong and weak bisimulation, observation equivalence, may and must preorder.
    Evaluation of dependability and performance properties: dependability modeling, model checking of continuous stochastic logic specifications.
    Proof of program correctness: basic methods (computational and structural induction). Formalization of program correctness. Correctness of simple low-level programs (partial correctness and termination). Correctness of simple programs written in structural languages. The role of theorem proving, symbolic execution, abstract interpretation.
    4. Validation and testing: Software testing techniques. Fault models. Specification based (functional) and structure based test design. Test quality metrics.
    Testing strategies and test processes. Software unit testing, isolation techniques. Integration testing and system testing. Testing time dependent behavior.
    Testing object-oriented software. Inheritance, state and thread dependent test coverage. Statistical testing in OO software.
    Model based test generation techniques using behavior models and formal specification.

    9. Method of instruction Lectures.
    10. Assessment Oral exam at the end of the semester. Submission of homework assignments and its presentation is a prerequisite.
    11. Recaps The homework assignment can be submitted during the repetition period.
    13. References, textbooks and resources
    Presentation slides available on the web page of the course.
    G. G. Schulmeyer, G. R. MacKenzie: Verification and Validation of Modern Software-Intensive Systems. Prentice Hall, 2000.
    D. Peled: Software Reliability Methods. Springer-Verlag, 2001.
    E. M. Clarke, O. Grumberg, D. Peled: Model Checking. MIT Press, 2000.
    G. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991.

    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
    Total150
    15. Syllabus prepared by
    Dr. István Majzik, Associate Professor, BME MIT
    Dr. András Pataricza, Professor, BME MIT