Редактирование: ВПнМ, 02 лекция (от 15 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | '''Оригинальная презентация:''' http://savenkov.lvk.cs.msu.su/mc/lect2.pdf<br /> | ||
'''Диктофонная запись:''' http://esyr.org/lections/audio/verification_2008_summer/verification_08_02_15.ogg | '''Диктофонная запись:''' http://esyr.org/lections/audio/verification_2008_summer/verification_08_02_15.ogg | ||
Можно либо изначально построить модель, либо в процессе разработки. | Можно либо изначально построить модель, либо в процессе разработки. | ||
- | На первом этапе выделяем из требований классы свойств, и по описанию системы и классам св-в строим модель. после этого описываем конкретные свойства, которые проверяем в процессе верификации. Подаём модель и св-ва на вход верификатора и | + | На первом этапе выделяем из требований классы свойств, и по описанию системы и классам св-в строим модель. после этого описываем конкретные свойства, которые проверяем в процессе верификации. Подаём модель и св-ва на вход верификатора и о проверяет. Дальше может быть несколько вариантов: |
* Свойство выполняется. Если модель корректна, то программа корректна. | * Свойство выполняется. Если модель корректна, то программа корректна. | ||
* Верификация не останавливается тогда, когда мы этого хотим. Это означает, что слишком сложная модель. Надо останавливать процесс вериф. и модернизировать модель | * Верификация не останавливается тогда, когда мы этого хотим. Это означает, что слишком сложная модель. Надо останавливать процесс вериф. и модернизировать модель | ||
Строка 12: | Строка 11: | ||
** Ошибка есть в описании. Исправляем программу | ** Ошибка есть в описании. Исправляем программу | ||
- | + | Вериф. автоматизирована, но автоматизир. только сам процесс и частично построение модели. Но участие человека довольно велико. Построение модели, анализ результатов верификатора. | |
== Построение модели == | == Построение модели == | ||
- | Модель нельзя построить без | + | Модель нельзя построить без св-в, которым она должна удовлетворять. |
Примеры классов свойств: | Примеры классов свойств: | ||
Строка 30: | Строка 29: | ||
У нас есть система, строим более простую модель, на ней проверяем свойства. Причин строить модели две: | У нас есть система, строим более простую модель, на ней проверяем свойства. Причин строить модели две: | ||
- | * Программа, написанная на инженерном ЯП, предназначена для того, чтобы данные обрабатывать | + | * Программа, написанная на инженерном ЯП, она предназначена для того, чтобы данные обрабатывать |
- | * Абстракция от лишних | + | * Абстракция от лишних осстояний |
- | Мы хотим | + | Мы хотим уменьш. пространство сост. Что же такое сост. программы? |
- | * Состояние программы --- какой оператор выполняется, что записано в память (не только переменные, но и любые ресурсы, с которыми работает программа) | + | * Состояние программы --- какой оператор выполняется, что записано в память (не только переменные, но и любые ресурсы, с которыми работает программа) |
- | + | Необх. отметить, что если мы говорим про отдельные программы, то не так просто сказать, что такое состояние. Поэтому, когда мы говорим о сост. программы, мы прибегаем к абстракции. Состояние атомов, из которых создан компьютер, нам неинтересно, нужно провести грань. Состояние всегда связано с моделью программы. | |
Есть три переменных и 7 операторов --- 7*2^96 состояния. | Есть три переменных и 7 операторов --- 7*2^96 состояния. | ||
- | При этом, не все эти состояния по ходу порграммы достижимы. Число достижимых | + | При этом, не все эти состояния по ходу порграммы достижимы. Число достижимых сост. меньше, чем потенциальных, и нужно понимать, что просто смотря, анализируя текст программы, мы не можем оценить достиж. сост, поскольку эта задача алгоритмически неразрешима. |
второе число --- 6 * 3 * 2^64 | второе число --- 6 * 3 * 2^64 | ||
- | Первая задача, которую мы получим по курсу --- будет прислан текст программы на С, и нужно будет оценить число потенциальных и | + | Первая задача, которую мы получим по курсу --- будет прислан текст программы на С, и нужно будет оценить число потенциальных и дост. состояний, оценка должна быть обоснованная. По этому поводу лектор просит до след. среды написать на адрес model-checking@cs.msu.su, ФИО и группу и попросить дать порграмму. Если есть старосты групп, лектор просит прислать список групп |
- | Прежде чем говорить о моделировании, нужно поговорить о модели программ. Если говорить о языке С, то в качестве примера | + | Прежде чем говорить о моделировании, нужно поговорить о модели программ. Если говорить о языке С, то в качестве примера рассм. программу, подсчитывающую количество строк. У этой программы может быть очень большое число состояний, посмотрим, как её можно упростить: |
* Неважны имя файла | * Неважны имя файла | ||
* Отладочный вывод | * Отладочный вывод | ||
Строка 55: | Строка 54: | ||
В результате увидим, что файл не закрываем. | В результате увидим, что файл не закрываем. | ||
- | Модель --- упрощённое описание реальности. С явлением может быть связано несколько моделей, и каждая может отражать своё свойство. У дома может быть много разных схем,если все свалить в одну, то в ней будет трудно разобраться, поэтому они разделены. Кроме того, | + | Модель --- упрощённое описание реальности. С явлением может быть связано несколько моделей, и каждая может отражать своё свойство. У дома может быть много разных схем,если все свалить в одну, то в ней будет трудно разобраться, поэтому они разделены. Кроме того, электреку план водоснабжения может не сильно помочь, то есть модель должна быть адекватна. |
Соответственно, модель должна быть простой, корректной, адекватной | Соответственно, модель должна быть простой, корректной, адекватной | ||
Строка 94: | Строка 93: | ||
=== Размеченные системы переходов (LTS) === | === Размеченные системы переходов (LTS) === | ||
- | Та структура, которая | + | Та структура, которая заадёт пространство нашей модели. |
- | TS = <S, Act, <math>\ | + | TS = <S, Act, <math>\upper...{\rarr}{a}</math>,s_0, AP, L> |
- | У нас нет | + | У нас нет сост., из которых никуда нельзя перейти, если есть что-то подобное, то там возникает петля с невидимым действием тау. Есть две школы. часть людей, что часть состояний (завершающие) должно быть нетотальным, другие говорят, что состояние заверх. наблюдаемое и не происх. наблюдаемых действий, то там происходит ненабл. действие. |
* S --- множество состояний | * S --- множество состояний | ||
Строка 118: | Строка 117: | ||
=== Детерминизм === | === Детерминизм === | ||
- | Если у всех | + | Если у всех сост. нашей сист переходов есть только один потомок, то у нас система детерминированная. Иначе недетерм. |
Недетрминизм --- это фича | Недетрминизм --- это фича | ||
Строка 124: | Строка 123: | ||
Позволяет заменить условие недетерм. порядком вып., что позволяет строить модели. | Позволяет заменить условие недетерм. порядком вып., что позволяет строить модели. | ||
- | + | Нед. полезен для: | |
* | * | ||
* | * | ||
* | * | ||
- | Мы наблюдае не за | + | Мы наблюдае не за сост., а за изменением... |
=== Достижимость === | === Достижимость === | ||
- | Чтобы посчитать достижимость, нужно | + | Чтобы посчитать достижимость, нужно отслеить все фрагм. вычислений. |
=== Трассы === | === Трассы === | ||
- | + | Послдовательность разметки состояний. Мы фокусируемся на набл. свойствах системы. Свойства описываются атомар. предикатами | |
- | === Свойства | + | === Свойства лин. времени === |
- | Проверять мы можем | + | Проверять мы можем св-ва линейного времени. СЛВ определяет мн-во трасс, можно сказать, что оно принадл. мн-ву трасс. |
- | Система переходов | + | Система переходов удовл. свойству лин. времени,если система трасс сист. переходов. включается в сист. трасс свойства. |
=== Абстракция === | === Абстракция === | ||
- | + | Формальноеописание отнош. абстр. Трассу можно представить как интерпретацию: Множ. нат числе, отношение порядка и разметка кси, она для каждого порядкового номера говорит, что заданный в нём предикат истинный или ложен. | |
- | + | Рассм. две трассы, нам надо опр., что они связ. отн. абстр. Эти две трассы имеют разные функции ращметки (у одной модет быть больше, у другой меньше), кроме того, сост. могут соотв. жл-ты трассы с разным номером. Будем говорить, что одна трасса явл. абстракцией другой, если множество набл предикатов первой явл. подмножеством множества второй, сохр. св-ва част. порядка и определно отображ. и если какой-то предикат набл. в абстр. трассе, то знач. у него должно быть точно такое же, ка к и в детальной. | |
Пример: | Пример: | ||
- | мы | + | мы рассм. свойства p и q, и есть предикаты p, q, r... |
- | + | Возн. вопрос, как строить системы перезодов, которые генерируют трассы, которые удовл. отн. абстракции. | |
- | Пусть есть | + | Пусть есть мсистема, модель, свойство ЛВ. Если свойство выполн. на модели, то оно выполн. на системе. Мы може переформ. это усл. как ограничение на трассы. То есть, для любой трассы, которую может сгенер. система, существует такая, которая может сген модель такую, что она явл. абстракцией системы. Если свойство вып. на всех трассах модели, то, поскольку каждой трассе сист. соотв. трасса модели, то свойство вып. на трассах системы, и система корректна. Вопрос, как такое условие проверить, поскольку оно, во общем в соотв. с этим опр., потребует большое кол-во ресурсов. Давайте сформулируем достаточное условие: |
- | Пусть у нас есть система переходов исходной программы и модели. Чем они отл.: в модели прост. сост. меньше, алфавит действий меньше, в модели другое отн. переходов, другой алфавит предикатов, соотв. поменяется разметка. Мы поменяли всё. Если абстрактно поменяяем как угодно, то всё испортится. Наложим условие, как менять: множество состояний модели (первое условие в прямоугольнике лишнее), но вот алфавит предикатов модели совершенно точно включ. в алфавит системы, .... На отобрадение накл. ограничение, что нач. сост. системы должно отобр. в нач. сост. модели. Условие на сист. переходов: (Act' ∈ Act) каждому переходу из системы переходов системы должен | + | Пусть у нас есть система переходов исходной программы и модели. Чем они отл.: в модели прост. сост. меньше, алфавит действий меньше, в модели другое отн. переходов, другой алфавит предикатов, соотв. поменяется разметка. Мы поменяли всё. Если абстрактно поменяяем как угодно, то всё испортится. Наложим условие, как менять: множество состояний модели (первое условие в прямоугольнике лишнее), но вот алфавит предикатов модели совершенно точно включ. в алфавит системы, .... На отобрадение накл. ограничение, что нач. сост. системы должно отобр. в нач. сост. модели. Условие на сист. переходов: (Act' ∈ Act) каждому переходу из системы переходов системы должен соотв. переход в модели. |
Пока огр. таким опр. | Пока огр. таким опр. | ||
- | Есть изьян в этом условии: можно построить такую модель, что нарушим | + | Есть изьян в этом условии: можно построить такую модель, что нарушим доно из свойств. |
- | Можно назвать это | + | Можно назвать это усл. условно правильным. |
Если кто-то хочет, может найти. | Если кто-то хочет, может найти. | ||
- | Если | + | Если посм. расп., то увидим разные практикумы. У СП два практикума. А у АСВК практикума Петровского нет. |
{{ВПнМ}} | {{ВПнМ}} | ||
{{Lection-stub}} | {{Lection-stub}} |