Редактирование: ВПнМ, 02 лекция (от 15 февраля)

'''Оригинальная презентация:''' http://savenkov.lvk.cs.msu.su/mc/lect2.pdf<br />

На первом этапе выделяем из требований классы свойств, и по описанию системы и классам св-в строим модель. после этого описываем конкретные свойства, которые проверяем в процессе верификации. Подаём модель и св-ва на вход верификатора и он проверяет. Дальше может быть несколько вариантов:

Верификация автоматизирована, но автоматизирован только сам процесс и частично построение модели. Участие человека довольно велико:построение модели, анализ результатов верификатора.

Модель нельзя построить без свойств, которым она должна удовлетворять.

* Программа, написанная на инженерном ЯП, предназначена для того, чтобы данные обрабатывать

* Абстракция от лишних состояний

Мы хотим уменьшить пространство состояний. Что же такое состояние программы?

* Состояние программы --- какой оператор выполняется, что записано в память (не только переменные, но и любые ресурсы, с которыми работает программа).

Необходимо отметить, что если мы говорим про отдельные программы, то не так просто сказать, что такое состояние. Поэтому, когда мы говорим о состоянии программы, мы прибегаем к абстракции. Состояние атомов, из которых создан компьютер, нам неинтересно, нужно провести грань. Состояние всегда связано с моделью программы.

При этом, не все эти состояния по ходу порграммы достижимы. Число достижимых состояний меньше, чем потенциальных, и нужно понимать, что просто смотря, анализируя текст программы, мы не можем оценить достижимые состояния, поскольку эта задача алгоритмически неразрешима.

Первая задача, которую мы получим по курсу --- будет прислан текст программы на С, и нужно будет оценить число потенциальных и достижимых состояний, оценка должна быть обоснована. По этому поводу лектор просит до следующей среды написать на адрес model-checking@cs.msu.su, ФИО и группу и попросить дать порграмму. Если есть старосты групп, лектор просит прислать списки групп.

Прежде чем говорить о моделировании, нужно поговорить о модели программ. Если говорить о языке С, то в качестве примера рассмотрим программу, подсчитывающую количество строк. У этой программы может быть очень большое число состояний, посмотрим, как её можно упростить:

Модель --- упрощённое описание реальности. С явлением может быть связано несколько моделей, и каждая может отражать своё свойство. У дома может быть много разных схем,если все свалить в одну, то в ней будет трудно разобраться, поэтому они разделены. Кроме того, электрику план водоснабжения может не сильно помочь, то есть модель должна быть адекватна.

Та структура, которая задаёт пространство нашей модели.

У нас нет состояний, из которых никуда нельзя перейти, если есть что-то подобное, то там возникает петля с невидимым действием тау. Есть две школы: часть людей, что часть состояний (завершающие) должно быть нетотальными, другие говорят, что состояние завер. наблюдаемое и не происх. наблюдаемых действий, то там происходит ненабл. действие.

Если у всех состояний нашей системы переходов есть только один потомок, то у нас система детерминированная. Иначе недетерминированная.

Недетерминизм полезен для:

Мы наблюдае не за состоянием, а за изменением...

Чтобы посчитать достижимость, нужно отследить все фрагменты вычислений.

Последовательность разметки состояний. Мы фокусируемся на наблюдаемых свойствах системы. Свойства описываются атомарными предикатами.

=== Свойства линейного времени (СЛВ)===

Проверять мы можем свойства линейного времени. СЛВ определяет множество трасс, можно сказать, что оно принадлежит множеству трасс.

Система переходов удовлетворяет свойству линейного времени,если система трасс системы переходов включается в систему трасс свойства.

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

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

мы рассмотрим свойства p и q, и есть предикаты p, q, r...

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

Пусть есть система, модель, свойство ЛВ. Если свойство выполняется на модели, то оно выполняется на системе. Мы тоже переформолируем это условие как ограничение на трассы. То есть, для любой трассы, которую может сгенерировать система, существует такая, которая может сгенерировать модель такую, что она является абстракцией системы. Если свойство выполняется на всех трассах модели, то, поскольку каждой трассе системы соответствует трасса модели, то свойство выполняется на трассах системы, и система корректна. Вопрос, как такое условие проверить, поскольку оно, вообщем в соотв. с этим опр., потребует большое количество ресурсов. Давайте сформулируем достаточное условие:

Пусть у нас есть система переходов исходной программы и модели. Чем они отл.: в модели прост. сост. меньше, алфавит действий меньше, в модели другое отн. переходов, другой алфавит предикатов, соотв. поменяется разметка. Мы поменяли всё. Если абстрактно поменяяем как угодно, то всё испортится. Наложим условие, как менять: множество состояний модели (первое условие в прямоугольнике лишнее), но вот алфавит предикатов модели совершенно точно включ. в алфавит системы, .... На отобрадение накл. ограничение, что нач. сост. системы должно отобр. в нач. сост. модели. Условие на сист. переходов: (Act' &isin; Act) каждому переходу из системы переходов системы должен соответствовать переход в модели.

Есть изьян в этом условии: можно построить такую модель, что нарушим одно из свойств.

Можно назвать это условие условно правильным.

Если посмотреть расписание, то увидим разные практикумы. У СП два практикума. А у АСВК практикума Петровского нет.