Program verification and analysis
Description: The course gives an idea of modern software verification technologies used in the development of complex and fault-tolerant software systems. The course is based on the methods of testing software systems. It covers the issues of building a test environment, planning a test system, analyzing and detecting defects in the program code of the system under test, integration and system testing, and general aspects of user interface testing.
Amount of credits: 7
Пререквизиты:
- Information Systems Programming Tools
Course Workload:
| Types of classes | hours |
|---|---|
| Lectures | 30 |
| Practical works | |
| Laboratory works | 30 |
| SAWTG (Student Autonomous Work under Teacher Guidance) | 60 |
| SAW (Student autonomous work) | 90 |
| Form of final control | Exam |
| Final assessment method |
Component: Component by selection
Cycle: Profiling disciplines
Goal
- study of the basic principles and methods of software verification; acquisition of skills necessary for the practical application of methods of verification and analysis of programs
Objective
- obtaining basic knowledge about the software verification and analysis process
- formation of practical skills for self-identification, development, documentation, modification and planning of software requirements
Learning outcome: knowledge and understanding
- concepts and ideas on which program verification methods are based
Learning outcome: applying knowledge and understanding
- be able to organize the processes of collecting, analyzing, verifying and documenting the requirements imposed by stakeholders during the implementation of IT projects;
- own the methods and models used to develop and analyze requirements
Learning outcome: formation of judgments
- form judgments about the meaning and consequences of their professional activities, taking into account social, professional and ethical positions
Learning outcome: communicative abilities
- interpersonal and group communication skills for business interaction within IT projects
Learning outcome: learning skills or learning abilities
- develop learning skills that contribute to professional and personal development, professional development in the field of information technology
Teaching methods
- технологии проектно-ориентированного обучения
Assessment of the student's knowledge
Teacher oversees various tasks related to ongoing assessment and determines students' current performance twice during each academic period. Ratings 1 and 2 are formulated based on the outcomes of this ongoing assessment. The student's learning achievements are assessed using a 100-point scale, and the final grades P1 and P2 are calculated as the average of their ongoing performance evaluations. The teacher evaluates the student's work throughout the academic period in alignment with the assignment submission schedule for the discipline. The assessment system may incorporate a mix of written and oral, group and individual formats.
| Period | Type of task | Total |
|---|---|---|
| 1 rating | лабораторная работа 1 | 0-100 |
| лабораторная работа 2 | ||
| 2 rating | лабораторная работа 3 | 0-100 |
| лабораторная работа 4 | ||
| Total control | Exam | 0-100 |
The evaluating policy of learning outcomes by work type
| Type of task | 90-100 | 70-89 | 50-69 | 0-49 |
|---|---|---|---|---|
| Excellent | Good | Satisfactory | Unsatisfactory | |
| Работа на лабораторных занятиях | выполнил лабораторную работу в полном объеме с соблюдением необходимой последовательности действий; в ответе правильно пишет код; правильно выполняет анализ ошибок. При ответе на вопросы правильно понимает сущность вопроса, дает точное определение и истолкование основных понятий; сопровождает ответ новыми примерами, умеет применить знания в новой ситуации; может установить связь между изучаемым и ранее изученным материалом, а также с материалом, усвоенным при изучении других дисциплин. | выполнил требования к оценке «5», но допущены 2-3 недочета. Ответ обучающегося на вопросы удовлетворяет основным требованиям к ответу на 5, но дан без применения знаний в новой ситуации, без использования связей с ранее изученным материалом и материалом, усвоенным при изучении других дисциплин; допущены одна ошибка или не более двух недочетов, обучающийся может их исправить самостоятельно или с небольшой помощью преподавателя. | выполнил работу не полностью, но не менее 50% объема практической работы, что позволяет получить правильные результаты и выводы; в ходе проведения работы были допущены ошибки. При ответе на вопросы обучающийся правильно понимает сущность вопроса, но в ответе имеются отдельные проблемы в усвоении вопросов курса, не препятствующие дальнейшему усвоению программного материала; допущено не более одной грубой ошибки и двух недочетов | выполнил работу не полностью или объем выполненной части работ не позволяет сделать правильных выводов. При ответе на вопросы демонстрирует не владение основными знаниями и умениями в соответствии с требованиями программы; допущены больше ошибок и недочетов, чем необходимо для оценки 3 или не может ответить ни на один из поставленных вопросов. |
| экзамен | демонстрирует системные теоретические знания, владеет терминологией, логично и последовательно объясняет сущность явлений и процессов, делает аргументированные выводы и обобщения, приводит примеры, показывает свободное владение монологической речью и способность быстро реагировать на уточняющие вопросы | демонстрирует прочные теоретические знания, владеет терминологией, логично и последовательно объясняет сущность, явлений и процессов, делает аргументированные выводы и обобщения, приводит примеры, показывает свободное владение монологической речью, но при этом делает несущественные ошибки, которые исправляет самостоятельно или при незначительной коррекции преподавателем | демонстрирует неглубокие теоретические знания, проявляет слабо сформированные навыки анализа явлений и процессов, недостаточное умение делать аргументированные выводы и приводить примеры, показывает недостаточно свободное владение монологической речью, терминологией, логичностью и последовательностью изложения, делает ошибки которые может исправить только при коррекции преподавателем. | демонстрирует незнание теоретических основ предмета, несформированные навыки анализа явлений и процессов, не умеет делать аргументированные выводы и приводить примеры, показывает слабое владение монологической речью, не владеет терминологией, проявляет отсутствие логичности и последовательности изложения, делает ошибки, которые не может исправить даже при коррекции преподавателем, отказывается отвечать на занятии |
Evaluation form
The student's final grade in the course is calculated on a 100 point grading scale, it includes:
- 40% of the examination result;
- 60% of current control result.
The final grade is calculated by the formula:
| FG = 0,6 | MT1+MT2 | +0,4E |
| 2 |
Where Midterm 1, Midterm 2are digital equivalents of the grades of Midterm 1 and 2;
E is a digital equivalent of the exam grade.
Final alphabetical grade and its equivalent in points:
The letter grading system for students' academic achievements, corresponding to the numerical equivalent on a four-point scale:
| Alphabetical grade | Numerical value | Points (%) | Traditional grade |
|---|---|---|---|
| A | 4.0 | 95-100 | Excellent |
| A- | 3.67 | 90-94 | |
| B+ | 3.33 | 85-89 | Good |
| B | 3.0 | 80-84 | |
| B- | 2.67 | 75-79 | |
| C+ | 2.33 | 70-74 | |
| C | 2.0 | 65-69 | Satisfactory |
| C- | 1.67 | 60-64 | |
| D+ | 1.33 | 55-59 | |
| D | 1.0 | 50-54 | |
| FX | 0.5 | 25-49 | Unsatisfactory |
| F | 0 | 0-24 |
Topics of lectures
- Основные понятия
- Место верификации в жизненном цикле ПО
- Методы верификации программного обеспечения
- Методы верификации программного обеспечения
- Формальные методы верификации
- Методы и инструменты дедуктивного анализа
- Формальные методы верификации
- Динамические методы верификации
- Тестирование
- Синтетические методы верификации
- Валидация
- Документация, сопровождающая процесс верификации
Key reading
- А.С. Камкин. Введение в формальные методы верификации программ. ИСП РАН, 2017
- Девянин П.Н., Кулямин В.В., Петренко А. К. Моделирование и верификация политик безопасности управления доступом в операционных системах. - Горячая Линия - Телеком. - 2024
- Гагарина Л.Г. Технология разработки программного обеспечения. - учебное пособие. - Москва: ИНФРА М, 2018
- Синицын, С. В. Верификация программного обеспечения : учебное пособие для СПО / С. В. Синицын, Н. Ю. Налютин. — Саратов : Профобразование, 2019. — 368 c. — ISBN 978-5-4488-0357-4. — Текст : электронный // Цифровой образовательный ресурс IPR SMART : [сайт]. — URL: https://www.iprbookshop.ru/86194.html (дата обращения: 22.01.2025).
- Синицын, С. В. Верификация программного обеспечения : учебное пособие / С. В. Синицын, Н. Ю. Налютин. — 3-е изд. — Москва : Интернет-Университет Информационных Технологий (ИНТУИТ), Ай Пи Ар Медиа, 2020. — 367 c. — ISBN 978-5-4497-0653-9. — Текст : электронный // Цифровой образовательный ресурс IPR SMART : [сайт]. — URL: https://www.iprbookshop.ru/97540.html (дата обращения: 22.01.2025).
Further reading
- Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ. Model Checking. М.: МЦНМО, 2002
- Р. Андерсон. Доказательство правильности программ. М.: Мир, 1982
- Карпович Е.Е. Методы тестирования и отладки программного обеспечения : учебник. Москва : МИСИС, 2020
- В.В. Кулямин. Методы верификации программного обеспечения http://panda.ispras.ru/~kuliamin/docs/VerMethods-2008-ru.pdf
