Надёжность ПО (All in one) (2014), страница 4
Описание файла
PDF-файл из архива "Надёжность ПО (All in one) (2014)", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 4 страницы из PDF
Атомарные высказывания, в терминахкоторых задаются свойства,присутствуют в разметке модели2. Из нарушения свойства на моделиследует, что оно нарушается и наисходной системе51Адекватность модели• Модель называется адекватной, если:1. AP APMнеобходимое условие (можно вычислить)2.MP достаточное условие (нельзя вычислить)• Определить адекватность при построениинельзя, можно лишь обнаружитьнесоответствие и исправить модель52Пример корректной абстракциисистемы переходовp = T,q = Tq=Tq=Taap = F,q = Faq=Fq=Fbbp = T,q = TTbq=ddp = F,q = TTp = T,q = Feccq=q=Tfq=T(P)cfefτeq=Fq=Fp = F,q = Tq=Tdττ(M1)(M2)53Пример – проверяемыесвойства• В любом вычислении встречаетсясостояние, когда p=T & q=T – ни одна измоделей не адекватна,• Для любого пути верно, что за любым q= Fрано или поздно встретится q= T – всемодели адекватны,• Между двумя состояниями с q= Fвстречается не более чем 3 состояния с q=T – модель М1 адекватна, М2 – нет.54Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремени55Спасибо за внимание!56НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 4:Временные автоматыВМиК МГУ им.
М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.1План лекции• Временной автомат:– Общее описание– Пример– Синтаксис– Семантика• Сеть временных автоматов:– Описание– Пример• Временные свойства (логика TCTL)Временной автомат• Описание, пригодное для моделирования ианализа (асинхронных) систем реальноговремени• Содержит конечное множество состоянийуправления• Дополнительно содержит таймеры,принимающие действительные значения• В структуре автомата отражено влияние таймеровна поведение системыПример временного автоматаМодель переключателя освещения• Содержит 3 состояния управления:• Off (выключено)• Light (обычное освещение)• Bright (яркое освещение)• Свет выключается при 100 секундах неактивности• Свет включается при нажатии на кнопку (press)• Яркий свет включается при двойном нажатии (двухнажатиях, отстоящих не более чем на 3 секунды)Пример временного автоматаТаймеры• x – таймер, принимающий действительныенеотрицательные значенияИнварианты• Инвариант – это необходимое условиеактивности состоянияКаналы связи• press? – внешнее событие нажатия кнопкивключенияПредусловия• Предусловие – это необходимое условиевыполнения переходаСброс таймеров• При выполнении перехода таймер можетбыть сброшенВременные ограничения• Элементарное временное ограничение:ETC ::= x op n | x – y op nop ::= < | | = | | >(x, y C, n Z)• Временное ограничение:TC ::= ETC | TC TC | TC TC | TC | (TC)• Элементарное инвариантное ограничение:ETC ::= x op nop ::= < | (x C, n Z)• Инвариантное ограничение:TC ::= ETC | TC TCСинтаксис временного автоматаВременной автомат – это система(C, A, L, l0, P, E), где••••••C – множество таймеровA – множество действийL – множество состояний управленияl0 – инициальное состояниеP : L TC – назначение инвариантовE L TC A 2C L – множество переходовКонфигурация автомата• Конфигурация автомата: (l, v)• l – состояние управления• v : C R+ - оценка таймеров• Начальная конфигурация: (l0, v0)• l0 – инициальное состояние автомата• v0(x) = 0 для всех таймеров x• Обозначения:• v+d, d R+: v+d(x) = v(x) + d• v[C’], C’ C: v[C](x) = 0 при x C; v[C](x) = v(x) иначе• v |= g: формула g истинна при значениях таймеров,определяемых оценкой vВычисление автоматаШаг вычисления автомата состоит в• Продвижении времени:• состояние управления не изменяется,• все таймеры продвигаются на константу d;• Выполнении перехода:• выбирается переход из l в l’,• состояние управления меняется на l’,• таймеры, которыми помечен переход, сбрасываются;После применения шага инварианты всехсостояний должны быть выполненыВычисление автомата• Продвижение времени: (l, v) d (l, v+d), если• l L ( v+d |= P(l) )• Выполнение перехода: (l, v) a (l’, v’), если••••(l, g, a, C’, l’) Ev |= gv’ = v[C’]v’ |= P(l’)• = d a• Вычисление:c1 c2 … cn …• Инициальное вычисление:• c1 – начальная конфигурация автоматаСинхронизация автоматов• Выделяются действия синхронизации:• Активные: a!• Пассивные: a?• Они соответствуют посылке и приемусигнала по каналу a• При выполнении перехода ссинхронизацией выбирается второйпереход с парной синхронизацией, и этидва перехода в различных автоматахвыполняются одновременноСеть временных автоматов• C, A – множество таймеров и множестводействий сети• Сеть – это совокупность автоматовN = (A1, A2, …, An), где• Ai = (C, A, Li, l0i, Pi, Ei) – временныеавтоматы• Сеть – это параллельная композицияавтоматов с синхронизацией типаhandshakeСемантика сети• Конфигурация: (l, v)• l = (l1, l2, …, ln) – вектор управляющихсостояний автоматов сети• v : C R+ – оценка таймеров• Начальная конфигурация: (l0, v0)• l0 – вектор начальных состояний автоматов• v0(x) = 0 для всех таймеров x• Обозначение:• l[i l’] – вектор, полученный из l заменой i-йкомпоненты на l’Семантика сети• Правила продвижения времени и выполнения переходаобобщаются естественным образом (отношение )• Правило выполнения переходов с синхронизацией:(l, v) (l’, v’), где••••••l’ = l[i l’, j l’’]ij(li, !a, g’, C’, l’) Li, (lj, ?a, g’’, C’’, l’’) Ljv’ = v[C’ C’’]v |= g’ g’’l l’ ( v’ |= P(l) )• Вычисление сети:c1 c2 … cn …• Инициальное вычисление сети:• c1 – начальная конфигурация сетиПример сетиЗадача о викингах:• N викингов хотят перейти через мост• У каждого викинга своя максимальная скорость• Имеется один факел• Идти через мост можно только при факелеодному или вдвоем• Требуется перевести викингов через мост какможно быстрееПример сети• Автомат для i-го викинга• y[i] – уникальный для i-го викинга таймер• delay[i] заменяется на конкретную константу –минимальное время прохода по мостуПример сети• Временной автомат для факелаЛогика TCTL• Временное ограничение:CC ::= x op n | x – y op nop ::= < | | = | | >(x, y C; n Z)• Формула: ::= P | CC | z. | | | | AG | AF | EG | EF | A( U ) | E( U )Логика TCTL(упрощенный вариант)• Элементарный предикат:EP ::= Ai.l | x op n | x – y op nop ::= < | | = | | >(l Li; x, y C; n Z)• Формула: ::= EP | | | | AG | AF | EG | EF | A( U ) | E( U )• Обозначение:• N, c |= : формула выполняется вконфигурации c сети NЛогика TCTL(упрощенный вариант)••••••••N, ((l1, l2, …, ln), v) |= Ai.l li = lN, (l, v) |= x op n v |= x op nN, (l, v) |= x – y op n v |= x – y op nN, c |= AG в каждой конфигурации каждоговычисления, начинающегося в c, выполнена формула N, c |= AF хотя бы в одной конфигурации каждоговычисления, начинающегося в c, выполнена формула N, c |= EG N, c |= AF N, c |= EF N, c |= AG Соотношения для булевых связок определяютсяестественным образомПримеры временных свойств• Можно перевести всех викингов через мост завремя T (здесь time – таймер сети)EF(Viking[1].Right … Viking[n].Right time T)• Нельзя перевести викинга за время, меньшеевремени его перехода через мостAG (Viking[i].Right and time < delay[i])• Если факел был захвачен, рано или поздно онбудет освобожден (не выполняется)AG((Torch.Left Torch.Right) AF(Torch.Left Torch.Right))Спасибо за вниманиеНАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 5:Логика линейного времени(LTL)ВМиК МГУ им.
М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.1План лекции• Свойства безопасности и живучести• Логика линейного времени (LTL)• Свойства, инвариантные к прореживанию• Практические приёмы формулированиясвойств на LTLРассуждения о правильностипрограммы• Требования правильности задаются как утверждения овозможных или невозможных вариантах выполнениямодели,• рассуждения о вероятности не допускаются из соображенийстрогости доказательства;• Мы утверждаем, что некоторые варианты выполнениямодели• либо невозможны,• либо неизбежны;• Двойственность утверждений:• если что‐то неизбежно, то противоположное – невозможно,• если что‐то невозможно, то противоположное – неизбежно,• используя логику, можно переходить от одного к другому припомощи логического отрицания.Свойства безопасности и(автор – LeslieживучестиLamport)безопасность•«ничего плохогоникогда не произойдёт»;живучесть• пример: инвариант системы•«рано или позднопроизойдёт что‐тохорошее»;• пример: «отзывчивость»– (х всегда меньше y);–• задача верификатора – найтивычисления, которые ведут кнарушению свойствабезопасности (то «плохое»,которое никогда не должнопроизойти)если отправлен запрос,то рано или поздно будетсгенерирован ответ;• задача верификатора – найтивычисления, в которых это«хорошее» можетоткладываться добесконечностиНемного подробнее…• Свойства безопасности – самые простыесвойства («состояние, где истинно φ,недостижимо»).• Можно ли в рамках свойства безопасностисформулировать, что φ неизбежно?• «состояние, где истинно !φ, недостижимо»– не то, это слишком сильное свойство;• «состояние, где истинно φ, достижимо»– а это, наоборот, слишком слабое.Немного подробнее…• «φ неизбежно» – означает, что φобязательно достижимо;• для спецификации такой модальностии нужны свойства живучести.Классическая логика не можетописать утвержденияКлассическая логикаПримитивная модель истины: “черно-белая” модель, не существует степениуверенности-неуверенности, высказывания статичны, неизменны во времени неадекватна для высказываний о времениПример - (некоммутативность конъюнкции, A&B B&A):“Джону стало страшно и он убил” “Джон убил и ему стало страшно”“Джон умер и его похоронили” “Джона похоронили и он умер”“Джейн вышла замуж и родила ребенка” “Джейн родила ребенка ивышла замуж”В обычной логике высказываний не формализуются:Путин – наш президент (истинно только в какой-то период)Мы не друзья, пока ты не извинишьсяЕсли m поступит на вход в канал, то потом m появится на выходеКаждый запрос к лифту c произвольного этажа, поступивший в любой моментвремени, будет когда-нибудь в будущем удовлетворенЭлементарные (атомарные) утверждения о событиях обычно истинны в одинмомент времени и ложны в другой!Утверждения о событиях, происходящих в разные моменты времени, нельзякорректно выразить в обычной логике7Темпоральная логикаОпределение TL - это любая логическая система, которая позволяет, невводя явно понятие времени, формализовать утверждения, истинностькоторых изменяется со временем.