Лекция 3. Системы переходов (LTS). Корректность и адекватность LTS модели (1158512)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 3:Системы переходов (LTS). Корректность иадекватность LTS моделиВМиК МГУ им. М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.План лекции•••••••Система понятий, используемых в курсеРазмеченные системы переходов (LTS)Недетерминизм систем переходовПути, вычисления, трассыСвойства линейного времениКорректность моделиАдекватность модели2Итоги прошлой лекции• Свойства проверяются на состояниях иих последовательностях• Чтобы перебирать меньше состояний,исследуется не исходная система, а еёмодель• Модель должна быть простой,корректной и адекватной• В этом случае из правильности моделиследует правильность программы3Строго говоря…Если мы хотим доказать, что послепроверки правильности на модели впрограмме нет ошибок, то все этипонятия стоит сформулировать болеестрого4Строго говоря, всё должно бытьтак:Система(программа)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремени5Строго говоря, всё должно бытьтак:СистемаСистема(программа)(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремени6Различные представленияпрограммыt t lt l ll t lltint main(){printf(}Исходный кодпрограммыВзлетает,непадает,приземляетсяТребованияГраф программы(ACFG)□(TAKEOFF →(!FALL)U(LANDED))РазмеченнаясистемапереходовlllМножествовычисленийl l tt t ll ll lСпецификацияДопустимые(линейного времени) последовательностиатомарных высказыванийМножествотрассl=Tt=TtltЯзыкдопустимых7 трассРазмеченные системы переходов (LTS)8Пример LTS0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Состояние: (счётчик, x, y)9Пример LTS0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:SLСостояние: (счётчик, x, y)10Что включать в состояние• Набор атомарных высказываний APопределяется свойствами, которыенужно проверить• Изменение состояния связано сизменением выполнимости хотя быодного атомарного высказывания• Исходя из этого мы определяем, чтовключать в состояние программы• Главное – не «потерять» ни одногоизменения атомарных состояний11Пример LTS0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:SLСостояние: (счётчик, x, y)12Пример LTS0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:SLСостояние: (счётчик, x, y)13Пример LTS0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Состояние: (счётчик, x, y)14Что включать в состояние?В дальнейшем мы будем рассматривать«универсальное» определениесостояния, достаточное для проверкисвойств линейного времени илокализации их нарушения в описаниипрограммыСовокупность значения счётчиков управленияпоследовательных процессов и переменныхпрограммы15int p;Process Prod(){ProdПримерLTSConswhile(1)1.1:if(p < 2)1.2: p +=1;}process Cons() {while(1)2.1:if(p > 0)2.2: p -=1;}Состояние: (счётчик Prod,счётчик Cons, p)Часть состояний не показана(оператор беск.

цикла,стартовые состояния)Бесконечное количество вычислений, однакоразмеченная система переходов конечна16Недетерминизм• В ряде ситуаций шаг может сделатьлюбой из двух процессов, порядокдействий не определён• Недетерминизм = неопределённость• При построении LTS рассматриваются всевозможные варианты последовательностидействий17Недетерминизм• Вообще-то в природе довольно малонедетерминированных процессов• Да и те считаются недетерминированными,поскольку физические законы, по которымвыбирается действие, нам не известны• Недетерминизм появляется, как только мы незнаем причин выбора действия или считаемих несущественными18Недетерминизм• Порядок выполнения Prod и Cond наконкретном компьютере детерминирован иопределяется алгоритмом диспетчераоперационной системы и состоянием ресурсов• Для проверки правильности программы мырешили абстрагироваться от всего, кромеописания двух процессов• Итог – недетерминизм очерёдностивыполнения процессовПодробнее про разные виды недетерминизма –ниже19Недетерминизм – это фича!• Используется для:– моделирования параллельного выполненияпроцессов в режиме чередования(интерливинга)• позволяет абстрагироваться от алгоритмадиспетчеризации и скорости выполненияпроцессовProdConsELFSystem boardProcessor20Недетерминизм – это фича!• Используется для:– моделирования прототипа системы• не ограничивает будущую реализациюзаданным порядком выполнения операторовили конкретными входными данными21Недетерминизм – это фича!• Используется для:– построения абстракции реальной системы• для абстрагирования от деталей,несущественных для проверки свойств и дляпостроения модели по неполной информации22Недетерминизм в LTS• В LTS недетерминизм проявляется в видесостояний, из которых можно перейтиболее чем в одно состояниеAP  {a}aaaнедетерминизмдействийaнедетерминизматомарных высказыванийстрогие определения – далее23Недетерминизм в LTS• В LTS недетерминизм проявляется ввиде состояний, из которых можноперейти более чем в одно состояние??может произойти одноиз нескольких действийнаблюдатель не можетотличить два состояниястрогие определения – далее24Вспомогательные определенияПрямые потомки вершины sпо действию aпо всем действиямПрямые предки вершины sпо действию aпо всем действиям25Детерминизм26Путь• Конечным путём σ системы переходов TSназываетсятакаяпоследовательностьчередующихсясостоянийидействий,заканчивающаяся состоянием:• Бесконечным путём σ системы переходов TSназывается такая бесконечная последовательностьчередующихся состояний и действий:• Путь называется начальным, еслиs0  I27Вычисление• Путь называется максимальным, еслион бесконечен.• Вычислением системы переходов TSназывается начальный максимальныйпуть.28Примеры вычислений29Примеры вычислений30Примеры вычислений31Примеры вычислений32Примеры вычислений33Достижимость состояний• Состояние s  S называется достижимым (изначального) в системе переходов TS, еслисуществует начальный, конечный путь• Reach(TS) обозначает множество всехсостояний, достижимых в TS.34Трассы• Вычисление описывает последовательностьсостояний и действий; что происходит всистеме.

Требуется для описаниясемантики программы (позже).• Свойства корректности формулируются втерминах последовательностей значенийатомарных высказываний в состоянияхмодели.35• Система переходов:Трассы• Путь (фрагмент вычисления):• Трасса:фокусируемся на «наблюдаемом» поведении36Примеры трасс a  p  0вычислениетрасса a  p  0 трасса 2  b  p 1a!a !ba!a !b!aa!aab ba!a !ba!a !b37Свойства линейного времени• Атомарные высказывания:a - «находимся в точке отправки запроса»b - «находимся в точке приёма ответа»• Свойство:«после отправки запроса рано или позднополучим ответ»• Пример допустимых трасс:aØØØØØbØ…ØØØØØØØ…• Пример недопустимых трасс:aØØØØØØØ…aØØØØbaØ…38Свойства линейного времени• Свойство φ определяет набордопустимых трасс  (2 AP )• Свойство φ выполнимо на трассе σ:   • Система переходов TS удовлетворяетсвойству линейного времени φ:TS  Traces(TS )  TS(P)P39Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремени40Абстракция трасс• Представим трассу в форме интерпретации I:I (tr)  Ν, ,гдеN – множество натуральных чисел, – отношение порядка на N , а : N  AP  {T, } , и при этомn  0, p  AP (n, p)  T  p  L(s)41Абстракция трасс• Рассмотрим трассы tr и tr’ такие, что:• Будем говорить, что tr’ является(корректной) абстракцией tr ( tr  tr'), еслиAP'  AP : N  N : n, k  N n  k  (n)  (k)n  N , p  AP'  (n, p)   ' ((n), p)42Пример абстракции трассp=Tq=Fr=Fp=Tq=Fr=Tp=Fq=Fr=Fp=Fq=Tr=Tp =Fq =Tr=FAP={p,q,r}p=Tq=Fp=Tq=Fp=Fq=Fp=Fq=Tp=Fq=TAP’={p,q}p=Tq=Fp=Fq=Fp=Fq=TAP’={p,q}43Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремени44Условие корректности модели• Пусть P – система, φ – произвольноесвойство линейного времени.

(Корректной)моделью P называется такое М, что:если свойство выполняется на модели, тооно выполняется и на системе• Это выполняется тогда и только тогда,когда:для любой трассы исходной системы вмодели найдётся её корректнаяабстракция45Условие корректности модели• Пусть P – система, φ – произвольноесвойство линейного времени. (Корректной)моделью P называется такое М, что:M P позволяет проверять свойствапрограммы на её моделиопределение• Это выполняется тогда и только тогда,когда:tr Traces(TS(P))tr'Traces(TS(M )) :tr  tr'для проверки такого условия нужно рассмотретьвсе трассы исходной системыдопускает, что в моделибольше состояний46необходимое и достаточное условиеДостаточное условиекорректности• Какими же свойствами должна обладатьTS модели, чтобы быть корректной?– действиям и атомарным высказываниям моделидолжны быть сопоставлены действия и атомарныевысказывания системы,– каждому состоянию системы должно бытьсопоставлено состояние модели,– модель должна корректно сохранять множествоначальных состояний,– если в системе есть переход между двумясостояниями, в модели должен быть переход помежду соотв.

состояниями по соотв. действию,– соотв. состояния в модели и системе должны бытьразмечены атомарными высказываниями моделиодинаково.47Достаточное условиекорректности• Какими же свойствами должна обладатьTS модели, чтобы быть корректной?s  S, L'( (s))  L(s)  AP'48достаточное условиеПример корректной абстракциисистемы переходов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)49Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремени50Адекватность модели• Модель называется адекватной, если:1. Атомарные высказывания, в терминахкоторых задаются свойства,присутствуют в разметке модели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.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций