Министерство по развитию информационных технологий и коммуникаций республики узбекистан ургенчский филиал ташкентского университета информационных технологий имени мухаммада аль-хоразмий


Download 89.41 Kb.
bet2/3
Sana21.02.2023
Hajmi89.41 Kb.
#1216625
1   2   3
Bog'liq
Sillabus ВФМВП рус Abdullayev Anvar

Шифр и направление:

5330500 — Компьютерный инжиниринг (Компьютерный инжиниринг)

Учитель, который преподает этот предмет:

Абдуллаев Анвар Шухратбекович

anvar.abdullayev.1989@gmail.com
Телефон:
+998914221009

Место, где проводится урок:

Здание УФ

Продолжительность курса:




График личных консультаций учителя:

с понедельника по пятницу 10–00. 11–00

Распределение часов:

Обучение аудитории

Самостоятельное обучение



Лекция

Практика

90 ч.

30 ч.

60 ч.

Курс:

4

Семестр:

8

Форма образования:

очное

Кредит:

6

Форма оценивания:

Экзамен

Язык предмета:

русский


Краткая информация о курсе (КИ)

КИ1

В курсе «Формальные методы верификации программ» изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Курс включает в себя: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации требований (программные контракты и темпоральная логика линейного времени), методы доказательства корректности программ (метод индуктивных утверждений и метод фундированных множеств) и методы проверки моделей (теоретико-автоматный подход в явной и символической формах). В курсе также затрагиваются вопросы абстрактной интерпретации, разрешения ограничений, применения формальных методов в тестировании; даются сведения об инструментах Frama-C и Spin. Каждая тема лекций курса сопровождается практическими заданиями.


Предварительные требования курса

1.

Программирование

2.

База данных

3.

Структура данных и алгоритмы




Результаты обучения (РО)


Дается представление о корректности программ, т.е. их соответствии требованиям, и верификации — процессе проверки корректности. Делается обзор базовых методов верификации, включая как формальные (проверка эквивалентности, проверка моделей, дедуктивный анализ), так и неформальные (экспертиза, тестирование). Рассматривается общая схема
формальной верификации





На примере простого императивного языка — языка while — рассматриваются два метода формализации семантики языков программирования: операционная семантика (структурная операционная семантика Плоткина) и аксиоматическая семантика (дедуктивная система Хоара и метод Дейкстры, основанный на понятии слабейшего предусловия). Показывается, что программа — код на языке с формализованной семантикой — является математическим объектом, к которому применимы строгие логические рассуждения, в частности о его корректности или некорректности (конечно, при наличии формальных спецификаций требований)





Рассматриваются основы дедуктивной верификации последовательных программ: приводятся необходимые сведения о
дедуктивных системах и теории доказательств; дается представление о верификации программы как поиске доказательства условия корректности в дедуктивной системе, формализующей язык программирования (платформу). Показывается, что свойства циклов, так называемые инварианты, не выводимы из структуры программы. Задание инвариантов дает набросок доказательства корректности, проверку которого можно автоматизировать.





Рассматриваются элементы языка ACSL (ANSI/ISO C Specification Language), предназначенного для формальной спецификации (аннотирования) программ на языке C. Делается обзор платформы статического анализа Frama-C (Framework for Modular Analysis of C programs) и модуля Jessie, автоматизирующего дедуктивную верификацию C-программ на соответствие ACSL-спецификациям. Изложение базируется на примерах (подробное описание языка ACSL и основанных на нем инструментов доступно в соответствующей документации). Описанные средства могут использоваться в повседневной программистской практике.





Рассматривается один из первых подходов к формальной верификации программ — метод Флойда. Метод состоит из двух частей: метод индуктивных утверждений, предназначенный для доказательства частичной корректности, т.е. корректности без учета завершимости, и метод фундированных множеств, используемый для доказательства завершимости и полной корректности. Метод состоит в рассечении циклов, сопоставлении точкам сечения индуктивных утверждений (инвариантов), формулировке условий верификации и их доказательстве.





Рассматривается метод фундированных множеств, применяемый в паре с методом индуктивных утверждений для доказательства завершимости и полной корректности программ. Идея метода заключается в сопоставлении каждой точке сечения оценки — функции состояния, значение которой убывает при каждом прохождении через эту точку, но в то же время не может убывать бесконечно долго в силу характера изменений и ограничений, накладываемых соответствующим индуктивным утверждением. Если удается найти такие оценочные функции и доказать условия верификации, программа
завершается и, более того, является полностью корректной.





Рассматриваются вопросы автоматизации дедуктивной верификации программ, в частности вопросы автоматического синтеза инвариантов циклов. Задача синтеза оценочных функций отдельно не рассматривается — она может быть сведена к построению инвариантов у программ, расширенных счетчиками. Определяются основные понятия абстрактной интерпретации; приводятся примеры интерпретации в таких областях, как интервальная арифметика и теория выпуклых многогранников.





Рассматриваются основные подходы к автоматическому доказательству теорем, включая метод резолюций для логики высказываний и логики предикатов первого порядка. Вводятся понятия разрешающей процедуры и разрешимой теории, приводятся примеры разрешимых и неразрешимых теорий.





Рассматриваются параллельные программы — программы, состоящие из нескольких процессов, исполняемых совместно и взаимодействующих друг с другом через общие переменные. Семантика таких программ определяется с помощью парадигмы чередования процессов. Особое внимание уделяется так называемым реагирующим системам — программам особого типа, работающим в «бесконечном цикле» и реагирующим на события окружения путем исполнения тех или иных действий.





Рассматриваются базовые возможности языка PROMELA и основанного на нем инструмента SPIN. Язык PROMELA (PROcess MEta-LAnguage) предназначен для моделирования асинхронных параллельных систем. Инструмент SPIN (Simple Promela INterpreter) позволяет анализировать PROMELA-модели, в том числе устанавливать соответствие моделей LTL-
спецификациям, т.е. проверять, является ли модель (программа на языке PROMELA) моделью (в логическом понимании) заданной формулы LTL. Описанные средства могут быть использованы на практике при проектировании параллельных программ и реагирующих систем.





Рассматриваются вопросы адекватности моделирования программ структурами Крипке, в том числе вопросы выбора уровня абстракции данных и гранулярности действий. Дается представление о предикатной абстракции программ и адаптивном уточнении абстракции на основе контрпримеров — методе CEGAR (Counter Example Guided Abstraction Refinement). Рассматриваются базовые подходы к исследованию пространства состояний параллельной программы, позволяющие по моделям процессов строить модель всей программы.







Download 89.41 Kb.

Do'stlaringiz bilan baham:
1   2   3




Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan ©fayllar.org 2024
ma'muriyatiga murojaat qiling