Subject » BMEVIMMD052
Software Verification and Validation
Szoftver verifikáció és validáció
A tantárgyleírás hatályossága
Hatályosság kezdete:
2026. March 21.
Hatályosság vége:
—
| Subject name (Hungarian, English) |
Szoftver verifikáció és validáció
Software Verification and Validation
|
||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Subject code | BMEVIMMD052 | ||||||||||||
| Subject type | — | ||||||||||||
| Training Level | — | ||||||||||||
| Course types and hours (weekly/semester) |
|
||||||||||||
| Assessment type | vizsga | ||||||||||||
| Credits | 5 | ||||||||||||
| Subject coordinator |
DR. Majzik István
position: egyetemi docens
contact:
majzik.istvan@vik.bme.hu
|
||||||||||||
| Responsible department |
Mesterséges Intelligencia és Rendszertervezés Tanszék
|
||||||||||||
| Faculty | Villamosmérnöki és Informatikai Kar | ||||||||||||
| Subject website | http://www.mit.bme.hu/oktatas/targyak/vimmd052 | ||||||||||||
| Primary curriculum type | — | ||||||||||||
| Direct prerequisites – Strong prerequisite | none | ||||||||||||
| Direct prerequisites – Weak prerequisite | none | ||||||||||||
| Direct prerequisites – Parallel prerequisite | none | ||||||||||||
| Direct prerequisites – Milestone prerequisite | none | ||||||||||||
| Direct prerequisites – Exclusion | none |
Objectives
Programme
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).
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.
Learning outcomes
Ez a tantárgy a KKK rendeletben meghatározott, következő kompetenciák fejlesztését szolgálja:
Knowledge
No learning outcomes recorded.
Skills
No learning outcomes recorded.
Attitudes
No learning outcomes recorded.
Autonomy and responsibility
No learning outcomes recorded.
Oktatási módszertan
Lectures.
Tanulástámogató anyagok
Online források
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.
Recommended preliminary knowledge for completing the subject
Knowledge type competencies
(azon előzetes ismeretek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)
nincs
Skill type competencies
(azon előzetes képességek és készségek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)
nincs
Recommended (non-compulsory) preliminary competencies
(azon ajánlott (nem kötelező) előzetesen megszerzendő kompetenciák összessége, amelyek jelentősen hozzájárulnak a tantárgy eredményes teljesítéséhez)
nincs
General rules
Requirements:
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.
Additional possibilities:
The homework assignment can be submitted during the repetition period.
Assessment methods
In-term assessments
No detailed assessments provided.
Weight of in-term assessments
No weights provided.
Exam-period assessments
No detailed assessments provided.
Weight of exam elements
No weights provided.
Grade calculation
No grade thresholds provided.
Attendance requirements
No attendance requirements provided.
Rules for retake and resubmission
Not provided.
Short description
Not provided.
Detailed description
Not provided.
Recommended courses
Not provided.
Workload to complete the subject
No workload breakdown provided.
Validity of subject requirements
Requirements valid from:
—
Requirements valid until:
—
Curriculum placement
No curriculum placements recorded for this subject version.