Надёжность ПО (All in one) (2014), страница 4

PDF-файл Надёжность ПО (All in one) (2014), страница 4 Надёжность программного обеспечения (53223): Лекции - 7 семестрНадёжность ПО (All in one) (2014): Надёжность программного обеспечения - PDF, страница 4 (53223) - СтудИзба2019-09-18СтудИзба

Описание файла

PDF-файл из архива "Надёжность ПО (All in one) (2014)", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 4 страницы из PDF

Атомарные высказывания, в терминахкоторых задаются свойства,присутствуют в разметке модели2. Из нарушения свойства на моделиследует, что оно нарушается и наисходной системе51Адекватность модели• Модель называется адекватной, если:1. AP APMнеобходимое условие (можно вычислить)2.MP достаточное условие (нельзя вычислить)• Определить адекватность при построениинельзя, можно лишь обнаружитьнесоответствие и исправить модель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’’]ij(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 - это любая логическая система, которая позволяет, невводя явно понятие времени, формализовать утверждения, истинностькоторых изменяется со временем.

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5076
Авторов
на СтудИзбе
455
Средний доход
с одного платного файла
Обучение Подробнее