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

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 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.