Определения по курсу Верификация моделей программ (1161287)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Расшифровка цветовых обозначенийЧерное – взято из слайдов К.О. Савенкова 2010 года.Красное – взято из книги Э.М. Кларка по верификации.Синее – придумано мною или слито с esyr.org или рождено на форуме cmcspec.ru.Делали: SLenik (полностью лекции 1-3, частично 4 и 5), <вставьте свою фамилию>Лектор = Константин Олегович Савенков (слева)Что-то краткое по курсу «Верификация моделей программ»Этапы разработки программ: Анализ Проектирование Реализация Тестирование ЭксплуатацияВерификация – исследование и обоснование соответствия программы своей спецификации.Задача верификации в общем случае алгоритмически неразрешима!Методы верификацииАвтоматизируемость методов верификации Тестирование: автоматическое и автоматизированное Доказательство теорем: существенное участие человека Статический анализ: полностью автоматический для заданной области и свойства Верификация на моделях: участие человека при построении модели и при анализеконтрпримеровОбласти применения верификации на моделях Сетевые и криптографические протоколы Протоколы работы кэш-памяти Интегральные схемы Стандарты Встроенные системы Драйвера Вообще программы на СВерификацию ПО выполнять сложнее, чем верификацию аппаратуры, поскольку последняягораздо лучше структурирована.

К тому же параллельные программы зачастую работают васинхронном режиме – без глобальных синхронизирующих часов, что является одной из причинт.н. комбинаторного взрыва.Моделирование программМодель – упрощённое описание реальности, выполненное с определенной целью. с каждым объектом может быть связано несколько моделей каждая модель отражает свой аспект реальностиАспекты модели Простота – модель должна быть проще, чем реальность Корректность – не расходиться с реальностью Адекватность – соответствовать решаемой задачеПостроение модели1.

Формализация требований (постановка задачи моделирования)2. Выбор языка моделирования3. Абстракция системы до модели с учётом требованийМодель программы = множество состояний программы, тотальное множество переходов междусостояниями и функция, помечающая каждое состояние набором свойств, истинных в данномсостоянии.Состояние программы – совокупностью значений переменных программы и счетчиковуправления последовательных процессов.Состояние называетсяСостояние называется потенциальным, если соответствующее состояние допустимо в рамкахмодели программы.Состояние называется достижимым, если существует бесконечная последовательностьсостояний, каждое из которых получено из предыдущего посредством некоторого перехода, вкотором оно (состояние) встречается.В общем случае задача определения достижимости состояния алгоритмически неразрешима.Степень детализации (гранулярность) переходовПри построении переходов важно достичь их атомарности – добиться того, чтобы ни однонаблюдаемое состояние системы не являлось результатом выполнения всего лишь некоторойчасти переходов.Для этого избегаем двух крайностей: Не определяем переходы «чрезмерно крупно» (модель программы может не включатьнекоторые наблюдаемые состояния – при верификации ошибки могут быть пропущены). Не описываем программу «излишне подробно» (могут образовываться новые состояния,которых в реальной программе никогда не будут достигнуты – при верификации могутобнаружиться призрачные ошибки, которые никогда не случаются на практике)Формальное описание этапов верификацииВ ходе верификации применяются различные представления программыРазмеченная система переходов (LTS)〈где:→〉– множество состояний *конечное или счетное+– множество действий (где – невидимое действие) [конечное]→– тотальное отношение переходов.

Тотальность означает, что длякаждого состояниядолжно существовать такое состояние, что имеет место→ (или что из каждого состояния ведет какое-то действие)– множество начальных состояний– множество атомарных высказываний (некоторый набор свойств)– функция разметки (помечает каждое состояние множеством атомарныхвысказываний, истинных в данном состоянии).НедетерминизмВ общем виде определения нет, только синоним – неопределенность.Появляется в том случае, когда мы не знаем причин выбора действия или считаем ихнесущественными.Использование Моделирование параллельного выполнения процессов в режиме чередования(проверяем все возможные варианты параллельного выполнения с точностью досостояния) Моделирование прототипа системы (не ограничивает будущую реализацию заданнымпорядком выполнения операторов или конкретными входными данными) Построение абстракции реальной системы (абстрагируемся от деталей, несущественныхдля проверки свойств и построения модели по неполной информации)Недетерминизм в LTS – проявляется в виде состояний, из которых можно перейти более, чем водно состояния.Недетерминизм действий (может произойти одно из нескольких действий)Недетерминизм атомарных высказываний (наблюдатель не может отличить двасостояния)Строгое определение недетерминизма в LTSПрямые потомки вершины s(по действию a:) по всем действиям:Прямые предки вершины sпо действию a:по всем действиям:({( ))| →}(⋃{( ))| → }( )⋃〈〉 детерминированаРазмеченная система переходов→ По действиям тогда и только тогда, когда:и( ) По атомарным высказываниям тогда и только тогда, когда:и( ) ( )+Конечным путемсистемы переходов*называется такая последовательность чередующихсясостояний и действий, заканчивающихся состоянием:Бесконечным путемПримечание [S1]: Непонятно, где жеэто определение используется.

ИМХОоно вообще лишнеесистемы переходов, чтоПримечание [S2]: Формула сослайдов упрощена (т.к. Post(s) –множество, допускается и такая запись)Примечание [S3]: Аналогичнопредыдущему примечанию→называется такая последовательностьчередующихся состояний и действий:, что →Путь в системе переходов TS называется начальным, еслиПуть в системе переходов TS называется максимальным, если он бесконечен.Вычислением системы переходов TS называется начальный максимальный путь.Состояние называется достижимым (из начального) в системе переходов TS, если существуетначальный конечный путь, содержащий это состояние.( ) – обозначение множествадостижимых состояний в системе переходов TS.Трассадля путив системе переходов TS – последовательность множеств атомарныхвысказываний, записанных для каждого состояния пути в порядке следования состояний.Примечание [S4]: Просто инвариантзаписи со слайдовПримечание [S5]: инвариантСвойство линейного времени() определяет набор допустимых трасс Свойство выполнимо на трассе : Система переходов TS удовлетворяет свойству линейного времени( ), ( ):Абстракция трасс〉Представим трассу в форме интерпретации ( ) 〈 N – множество натуральных чисел– отношение порядка на N+, и при этом()( )→*〉〈〉+,+.Рассмотрим две трассы = 〈→*→*является корректной абстракцией (), если:1.(выбрали какие-то атомарные высказывания)( )2.→ , т.ч.( ) (придумали какую-то неубывающуюнатуральную функцию)()3.( ( ) ) (и при помощи этой функции перенумеровалисобытия, сохранив их порядок друг относительно друга)Условие корректности моделиПусть P – система, а– произвольное свойство линейного времени.

Корректной моделью Pназывается такая модель M, для которой верно: если свойство выполняется на модели M, тооно выполняется и на системе P.Это утверждение верно тогда и только тогда, когда для любой трассы исходной системы P вмодели M найдется ее корректная абстракция.Достаточное условие корректности модели〈1.2.3.→→〉〈〉→(отобрали какие-то действия)(и какие-то атомарные высказывания)( ) (придумали какую-то неубывающую натуральную функцию)( ) → ( ) (перенумеровали с ее помощью все отобранные состояния так,→чтобы переходы, которые были между отобранными состояниями, сохранились)( )5.( ( ))(и попросили, чтобы функция разметки каждое изотобранных состояний размечала только отобранными атомарными высказываниями)4.Адекватность моделиМодель называется адекватной, если(атомарные высказывания, в терминах которых задаются свойства,присутствуют в разметке модели)(из нарушения свойства на модели следует, что оно нарушается и наисходной системе)Верификация программы при помощи модели Нужно знать, как система устроена и как она должна быть устроена. Соответственно, нужно две нотации:o Описание поведения (устройства системы)o Описание требований (свойств правильности) Выбранная нотация гарантирует разрешимость любого свойства любой модели.Формальное представление программы1.

Граф, задающий структуру программы2. Статическая семантика – набор ограничений, которым должна удовлетворять программа3. Операционная семантика – понятие состояния программы, и изменение состояния в ходеработы программы.Примечание [S6]: В лекции неверно– единый абстрактный домен данных (базовый тип для всех типов данных, тождественноравен типу int)– множество переменных программы P.Функция означивания переменной→(возвращает тип переменной по ее имени)( ) – набор булевых условий над множеством .() – множество значений переменных.

Собственно, это и есть подстановка.()→Эффект –()Примечание [S7]: В слайдах Var –множество, – тоже. При этом(?!)Графы программ (статическая семантика)〈〉, где:→– множество точек, исходные (начальные) точки– множество действий→(( ))– отношение переходов,страж оператора()→() – функция эффекта( ) – начальное условиеозначает 〈Нотация: →〉( ) – это фактически→Принцип получения TS из PG Состояние: точка l + значение данных Начальное состояние: начальная точка + все значения данных, удовлетворяющие . Атомарные высказывания в TSo находимся в точке программыo значение переменной x принадлежит некоторому множеству , и это множествоявляется подмножеством множеств значений этой переменной( )Если →истинно в , то строим отношение переходов как 〈〉→〈()〉Система переходов графов программ TS(PG) над переменными описывается сигнатурой〉, где:( ) 〈→( ) (состояние: точка l + значение данных )*〈 〉+ (множество начальных состояний системы переходовописывается как множество состояний, в которых точка программы принадлежитначальным точкам, а на подстановках выполняется начальное условие графа программы)( ) (объединение множества точек программы и всевозможныхбулевых высказываний над переменными программы)(〈 〉) * + {( )|+ (состояния размечаются высказыванием о точкепрограммы, в которой мы находимся и всеми высказываниями из множествавсевозможных высказываний, которые верны в этой подстановке)→из взадается правилом: если →истинно в (в графе программы есть дугасо стражем и действием и в некоторой подстановке выполняется страж ), тостроим отношение переходов как 〈〉→〈()〉Чередование (интерливинг) ОбоснованиеЭффект от параллельного выполнение независимых действий α ипоследовательного выполнения в произвольном порядке Символьная запись) () )()((o– бинарный оператор чередованияo + – оператор недетерминированного выполненияo ; – оператор последовательного выполненияЧередование систем переходов〈〉Пусть→* + – две системы переходовравен эффекту от ихПримечание [S8]: Совершенное инепонятное про атомарныевысказывания, добавлены слова изesyr’аПримечание [S9]: Не пояснено вслайдахОпределим их чередованиекак 〈( )〉, а отношение перехода → определяется правилами:(→)→ ()→)→ (и()Чередование графов программ〈〉*Пусть→Графопределим как 〈Где отношение перехода определяется правилами→〈〉→ 〈〉иИ эффект( )→+→〉→〈(〉→ 〈)〉(), еслиПараллелизм и рандеву распределённые программы выполняются параллельно в распределённой программе нет разделяемых переменныхПередача сообщений в распределённых программах синхронная передача сообщений (рандеву, без буферизации) асинхронная передача сообщений (с буферизацией)Синхронный обмен сообщениями Процессы вместе выполняют синхронизированные действия Взаимодействие процессов - одновременноРандеву систем переходов* +〈→〉– набор синхронизированных действий.o действия из H должны быть синхронизированыo действия не из H независимы и могут чередоваться( )Тогда〈→ → определяется как:oинтерливинг для→:〈〉→〈〉и→〈〉→〈〉( )〉, где(в случае интерливинга мыдобавляем новые переходы в произвольном порядке, см.

рисунок ниже)Примечание [S10]: Я понимаю, чторисунок отражает несколько иное, но тутон дан для понимания получениясистемы переходов для случаянезависимых действийoрандеву для→:〈→〉→〈〉(а вот это – ключевой момент определения:переход из пары состояний происходит только в том случае, когда оба процессадолжны что-то делать одновременно – например, прием-передачу информации всинхронном режиме)Синхронный параллелизм〈→(→ Тогда〈→ определяется как:〉*+)→( )→→〈→〉→ 〈〉( )〉(тот же комментарий, что и для определения рандевусистем переходов, для случая рандеву)PromelaКлючевые моменты У моделей – конечное число состояний (потенциально бесконечные элементы моделей вPromela ограничены).o Гарантирует разрешимость верификацииo Не гарантирует конечное число вычислений Асинхронное выполнение процессовo Нет глобальных часовo По умолчанию отсутствует синхронизация разных процессов Недетерминированный поток управленияo Абстракция от деталей реализации Понятие выполнимости оператораo С любым оператором связаны понятия предусловия и эффектаo Оператор выполняется (производя эффект)только если выполнено предусловие, впротивном случае он заблокированo Пример: q?m – если канал не пуст, получаем из него сообщение, иначе ждем.o Присваивания и printf выполняются всегда.

Характеристики

Тип файла PDF

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

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лабораторной работы