Лекция 4. Временные автоматы (Лекции)
Описание файла
Файл "Лекция 4. Временные автоматы" внутри архива находится в папке "Лекции". PDF-файл из архива "Лекции", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 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))Спасибо за внимание.