Верификация и анализ программ
内容描述: Курс дает представление о современных технологиях верификации программного обеспечения, применяемых при разработке сложных и отказоустойчивых программных систем. Курс основан на методиках тестирования программных систем. Он охватывает вопросы построения тестового окружения, планирования системы тестов, анализа и обнаружения дефектов программного кода тестируемой системы, интеграционного и системного тестирования, общих аспектов тестирования пользовательских интерфейсов.
贷款数: 7
Пререквизиты:
- Программные средства информационных систем
*СomplexityDiscipline(zh-CN)*:
| *TypesOfClasses(zh-CN)* | *hours(zh-CN)* |
|---|---|
| *Lectures(zh-CN)* | 30 |
| *PracticalWork(zh-CN)* | |
| *LaboratoryWork(zh-CN)* | 30 |
| *srop(zh-CN)* | 60 |
| *sro(zh-CN)* | 90 |
| *FormOfFinalControl(zh-CN)* | экзамен |
| *FinalAssessment(zh-CN)* | экзамен |
零件: Компонент по выбору
循环次数: Профилирующие дисциплины
Цель
- изучение базовых принципов и методов верификации программного обеспечения; приобретение навыков, необходимых для практического применения методов верификации и анализа программ
Задача
- получение базовых знаний о процессе верификации и анализа программного обеспечения
- формирование практических навыков самостоятельного выявления, разработки, документирования, изменения и планирования требований к программному обеспечению
Результат обучения: знание и понимание
- концепции и идеи, на которых основаны методы верификации программ
Результат обучения: применение знаний и пониманий
- уметь организовывать процессы сбора, анализа, верификации и документирования требований, предъявляемых заинтересованными сторонами в ходе реализации IT проектов;
- владеть методами и моделями, используемыми для разработки и анализа требований
Результат обучения: формирование суждений
- формировать суждения о значении и последствиях своей профессиональной деятельности с учётом социальных, профессиональных и этических позиций
Результат обучения: коммуникативные способности
- навыки межличностной и групповой коммуникации для делового взаимодействия в рамках ИТ проектов
Результат обучения: навыки обучения или способности к учебе
- развивать навыки обучения, способствующие профессиональному и личностному развитию, повышению квалификации в области информационных технологий
*TeachingMethods(zh-CN)*
- технологии проектно-ориентированного обучения
*AssessmentKnowledge(zh-CN)*
Преподаватель проводит все виды работ текущего контроля и выводит соответствующую оценку текущей успеваемости обучающихся два раза в академический период. По результатам текущего контроля формируется рейтинг 1 и 2. Учебные достижения обучающегося оцениваются по 100-балльной шкале, итоговая оценка Р1 и Р2 выводится как средняя арифметическая из оценок текущей успеваемости. Оценка работы обучающегося в академическом периоде осуществляется преподавателем в соответствии с графиком сдачи заданий по дисциплине. Система контроля может сочетать письменные и устные, групповые и индивидуальные формы.
| *Period2(zh-CN)* | *TypeOfTask(zh-CN)* | *Total(zh-CN)* |
|---|---|---|
| 1 *Rating(zh-CN)* | лабораторная работа 1 | 0-100 |
| лабораторная работа 2 | ||
| 2 *Rating(zh-CN)* | лабораторная работа 3 | 0-100 |
| лабораторная работа 4 | ||
| *TotalControl(zh-CN)* | экзамен | 0-100 |
*PolicyAssignmentTask(zh-CN)*
| *TypeOfTask(zh-CN)* | 90-100 | 70-89 | 50-69 | 0-49 |
|---|---|---|---|---|
| Excellent | *Grade4(zh-CN)* | *Grade3(zh-CN)* | *Grade2(zh-CN)* | |
| Работа на лабораторных занятиях | выполнил лабораторную работу в полном объеме с соблюдением необходимой последовательности действий; в ответе правильно пишет код; правильно выполняет анализ ошибок. При ответе на вопросы правильно понимает сущность вопроса, дает точное определение и истолкование основных понятий; сопровождает ответ новыми примерами, умеет применить знания в новой ситуации; может установить связь между изучаемым и ранее изученным материалом, а также с материалом, усвоенным при изучении других дисциплин. | выполнил требования к оценке «5», но допущены 2-3 недочета. Ответ обучающегося на вопросы удовлетворяет основным требованиям к ответу на 5, но дан без применения знаний в новой ситуации, без использования связей с ранее изученным материалом и материалом, усвоенным при изучении других дисциплин; допущены одна ошибка или не более двух недочетов, обучающийся может их исправить самостоятельно или с небольшой помощью преподавателя. | выполнил работу не полностью, но не менее 50% объема практической работы, что позволяет получить правильные результаты и выводы; в ходе проведения работы были допущены ошибки. При ответе на вопросы обучающийся правильно понимает сущность вопроса, но в ответе имеются отдельные проблемы в усвоении вопросов курса, не препятствующие дальнейшему усвоению программного материала; допущено не более одной грубой ошибки и двух недочетов | выполнил работу не полностью или объем выполненной части работ не позволяет сделать правильных выводов. При ответе на вопросы демонстрирует не владение основными знаниями и умениями в соответствии с требованиями программы; допущены больше ошибок и недочетов, чем необходимо для оценки 3 или не может ответить ни на один из поставленных вопросов. |
| экзамен | демонстрирует системные теоретические знания, владеет терминологией, логично и последовательно объясняет сущность явлений и процессов, делает аргументированные выводы и обобщения, приводит примеры, показывает свободное владение монологической речью и способность быстро реагировать на уточняющие вопросы | демонстрирует прочные теоретические знания, владеет терминологией, логично и последовательно объясняет сущность, явлений и процессов, делает аргументированные выводы и обобщения, приводит примеры, показывает свободное владение монологической речью, но при этом делает несущественные ошибки, которые исправляет самостоятельно или при незначительной коррекции преподавателем | демонстрирует неглубокие теоретические знания, проявляет слабо сформированные навыки анализа явлений и процессов, недостаточное умение делать аргументированные выводы и приводить примеры, показывает недостаточно свободное владение монологической речью, терминологией, логичностью и последовательностью изложения, делает ошибки которые может исправить только при коррекции преподавателем. | демонстрирует незнание теоретических основ предмета, несформированные навыки анализа явлений и процессов, не умеет делать аргументированные выводы и приводить примеры, показывает слабое владение монологической речью, не владеет терминологией, проявляет отсутствие логичности и последовательности изложения, делает ошибки, которые не может исправить даже при коррекции преподавателем, отказывается отвечать на занятии |
*EvaluationForm(zh-CN)*
Итоговая оценка знаний обучающего по дисциплине осуществляется по 100 балльной системе и включает:
- 40% результата, полученного на экзамене;
- 60% результатов текущей успеваемости.
Формула подсчета итоговой оценки:
| И= 0,6 | Р1+Р2 | +0,4Э |
| 2 |
где, Р1, Р2 – цифровые эквиваленты оценок первого, второго рейтингов соответственно; Э – цифровой эквивалент оценки на экзамене.
Итоговая буквенная оценка и ее цифровой эквивалент в баллах:
Буквенная система оценки учебных достижений обучающихся, соответствующая цифровому эквиваленту по четырехбалльной системе:
| Оценка по буквенной системе | Цифровой эквивалент | Баллы (%-ное содержание) | Оценка по традиционной системе |
|---|---|---|---|
| A | 4.0 | 95-100 | Отлично |
| A- | 3.67 | 90-94 | |
| B+ | 3.33 | 85-89 | Хорошо |
| B | 3.0 | 80-84 | |
| B- | 2.67 | 75-79 | |
| C+ | 2.33 | 70-74 | |
| C | 2.0 | 65-69 | Удовлетворительно |
| C- | 1.67 | 60-64 | |
| D+ | 1.33 | 55-59 | |
| D | 1.0 | 50-54 | |
| FX | 0.5 | 25-49 | Неудовлетворительно |
| F | 0 | 0-24 |
Темы лекционных занятий
- Основные понятия. Верификация и валидация. Характеристики качества программного обеспечения
- Место верификации в жизненном цикле ПО. Каскадный, V-образный, спиральный жизненные циклы. Верификация различных артефактов жизненного цикла ПО. Международные стандарты, касающиеся верификации ПО
- Методы верификации программного обеспечения. Экспертиза. Оценка ПО по Фагану. Методы экпертиз. Методы анализа архитектуры ПО
- Методы верификации программного обеспечения. Статический анализ.
- Формальные методы верификации. Логико-алгебраические модели. Исполнимые модели. Модели промежуточного типа.
- Методы и инструменты дедуктивного анализа. логика Хоара. Метод Флойда
- Формальные методы верификации. Методы и инструменты проверки моделей. Методы и инструменты проверки согласованности
- Динамические методы верификации. Оценка характеристик качества ПО с помощью динамических методов. Верификационный мониторинг.
- Тестирование. Виды тестирования. методы тестирования. Критерии полноты тестирования.
- Синтетические методы верификации.Тестирование на основе моделей. Мониторинг формальных свойств ПО. Статический анализ формальных свойств. Синтетические методы генерации структурных тестов
- Валидация. Подходы валидации данных.
- Документация, сопровождающая процесс верификации. Планом верификации. Тест-требования, тест-план, отчет о выполнении тестирования.
Основная литература
- А.С. Камкин. Введение в формальные методы верификации программ. ИСП РАН, 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).
Дополнительная литература
- Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ. Model Checking. М.: МЦНМО, 2002
- Р. Андерсон. Доказательство правильности программ. М.: Мир, 1982
- Карпович Е.Е. Методы тестирования и отладки программного обеспечения : учебник. Москва : МИСИС, 2020
- В.В. Кулямин. Методы верификации программного обеспечения http://panda.ispras.ru/~kuliamin/docs/VerMethods-2008-ru.pdf
