lect05 (1158546)

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

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

Верификация программна моделяхЛекция №5Графы программ. Системы с каналамивзаимодействия. Синхронный иасинхронный параллелизмКонстантин Савенков (лектор)План лекции• Alternating Bit Protocol• Графы программ• Операционная семантика графовпрограмм:– последовательные процессы,– чередование,– разделяемые переменные,– синхронная и асинхронная передачасообщениюAlternating Bit Protocol(Bartlett и др., 1969)• Два процесса, отправитель и получатель;• К каждому сообщению добавляется один бит;• Получатель сообщает о доставке сообщения,возвращая бит отправителю;• Если отправитель убедился в доставкесообщения, он отправляет новое, изменяязначение бита;• Если значение бита не изменилось, получательсчитает, что идёт повтор сообщения.Модель на Promelamtype = {msg, ack};chan s_r = [2] of {mtype, bit};chan r_s = [2] of {mtype, bit};active proctype sender(){ bit seqno;do:: s_r!msg,seqno ->if:: r_s?ack,eval(seqno) ->seqno = 1 - seqno;:: r_s?ack,eval(1-seqno)fiod}active proctype receiver(){ bit expect, seqno;do:: s_r?msg,seqno ->r_s!ack,seqno;if:: seqno == expect;expect = 1 - expect::elsefiodmsg(0)ack(0)msg(1)ack(1)Считываем новое сообщениеСохраняем сообщениеИгнорируем сообщениеЗапускаем моделирование>./spin -u20 -c abp.pmlproc 0 = senderproc 1 = receiverq\p011s_r!msg,01.s_r?msg,02.r_s!ack,02r_s?ack,01s_r!msg,11.s_r?msg,12.r_s!ack,12r_s?ack,1------------depth-limit (-u20 steps) reached------------final state:------------#processes: 2queue 1 (s_r):queue 2 (r_s):20:proc 1 (receiver) line 19 "abp.pml"(state 7)20:proc 0 (sender) line7 "abp.pml"(state 7)2 processes created>Моделируем первые 20 шаговВерификация по умолчанию>./spin -a abp.pml> gcc -o pan pan.c>./pan(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claimassertion violationsacceptancecyclesinvalid end states- (none specified)+- (not selected)+State-vector 44 byte, depth reached 13, errors: 014 states, stored1 states, matched15 transitions (= stored+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)unreached in proctype senderline 15, state 10, "-end-"(1 of 10 states)unreached in proctype receiverline 27, state 10, "-end-"(1 of 10 states)>Чем и как проверяем?Какие свойства?Проделанная работаИспользуемая памятьОбнаруженнедостижимый код(процессы незавершаются)Графический интерфейс xspinФункция eval()Отображает текущее значение xна константу, которая служитограничением дляпринимаемых сообщенийch!msg(12)ch?msg(eval(x))Сообщение будет принято, если значение переменной x равно 12Графы программСхема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениРазличные представленияпрограммыt t lt l ll t lltintmain(){printf(}Исходный кодпрограммыВзлетает,непадает,приземляетсяТребованияГраф программы(ACFG)□(TAKEOFF→(!FALL)U(LANDED))РазмеченнаясистемапереходовlllМножествовычисленийl l tt t ll ll lСпецификацияДопустимые(линейного времени) последовательностиатомарных высказыванийМножествотрассl=Tt=TtltЯзыкдопустимых трассРазмеченные системы переходов(напоминание)• описывают поведение системы;• ориентированный граф: узлы – состояния,дуги – переходы;• состояние – счётчик управления + значенияпеременных программы;• переход (изменение состояния) –выполнение оператора программы.Размеченные системы переходов(напоминание)TS  S , Act , , I , AP, La• S – множество состояний,• Act – множество действий, τ – невидимое действие,a  S  Act  S – тотальное отношение• переходов,• I  S – множество начальных состояний,• AP – множество атомарных высказываний,• L : S  2 AP – функция разметки.Формальное представлениепрограммы• LTS – всевозможные состояния программы ипереходы между ними;• Однако модель строится в виде программы наспециальном языке;• Рассуждения о корректности необходимоперенести на текст программы-модели;• Для этого понятие описания программынеобходимо формализовать;• Формальное представление программы: графпрограммы и его семантика.Формальное представлениепрограммы1.

граф, задающий структуру программы;2. статическая семантика – наборограничений, которым должнаудовлетворять структура;3. операционная семантика – понятиесостояния программы и изменениесостояния в ходе работы программы.то, как по графу строится LTSВспомогательные определения• DP – единый абстрактный домен данныхbool z;mtype {M1,M2} m = M1;proctype EQ(byte x, byte y){if:: (x == y) -> z = true:: else -> z = falsefi}DP  intbool  intbyte  intmtype  intВспомогательные определения• VP Var – множество переменных(последовательной) программы P ,v• v VP , dom(v )  DP  DPbool z;mtype {M1,M2} m = M1;proctype EQ(byte x, byte y){if:: (x == y) -> z = true:: else -> z = falsefi}VMAX  {z, m, x, y}Вспомогательные определения• Функция означивания переменной: : VP  DP , v VP ,  (v )  DvPbool z;mtype {M1,M2} m = M1;proctype EQ(byte x, byte y){if:: (x == y) -> z = true:: else -> z = falsefi}Примеры: (m)  M1  mtype ( x )  3  byte ( z )  true  boolВспомогательные определения• Cond (VP ) – набор булевых условий над VP– формулы пропозициональной логикиp1 ∧ p2 ∨ p3– используются высказывания вида x  Xp1 ≡ -3 < x ≤ 5p2 ≡ m = M2p3 ≡ y < 2 * xВспомогательные определения• Эффект операторов формализуется какотображениеEffect : Act  Eval (Var)  Eval (Var)…x = 17;if:: y = -2:: y = 3fi;…x = y + 5;…Пусть   x  y  5,1,2 ( x )  17, 1 ( y )  2,2 ( y )  3ТогдаEffect ( ,1 )( x )  1 ( y )  5  3Effect ( ,1 )( y )  1 ( y )  2Effect ( ,2 )( x )  2 ( y )  5  8Effect ( ,2 )( y )  2 ( y )  3Графы программ(статическая семантика)PG  Loc, Act , Effect, , Loc0 , g0•Loc – множество точек, исходные точки Loc0  Loc ,•Act– множество действий,• Effect : Act  Eval (Var)  Eval (Var) – функция эффекта,•  Loc  (Cond(VP )  Act )  Loc – отношение перехода,• g0  Cond(VP ) – начальное условие,g:Нотация : l l ' обозначаетl , g ,  , l ' Пример графа программы0,?,?00: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:int x = 2;:x = 2;1,2,?1int y = 0;:y = 0;22,2,0x > 0x > 0:τ3x <= 0:τx -= 1;3,2,0:x -= 1;x > 03,1,1y += 1;y += 1;:y += 1;42,1,14,2,14,1,2x -= 1;2,0,2!(x > 0)55,0,2Пример графа программы00: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5::x = 2;0, 1, 2, 3, 4, 51:y = 0;2x > 0:τ3:y += 1;4x <= 0:τ5Loc:x -= 1;Act“x=2”, “y=0”,“y+=1”, “x-=1”, τEffectLoc0 "0"g0  ( x # )  ( y # )Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениКак из PG получить TS?• Основная идея – раскрутка– состояние: точка l + значение данных η– начальное состояние: начальная точка + всезначения данных, удовлетворяющие g0;• Атомарные высказывания и разметка:– высказывания вида: “в l” и “x∈D”, где D⊆dom(x);– состояние <l,η> размечается высказыванием “в l”и всеми высказываниями, истинными в η;g:• Если l  l ' и g истинно в η, тоl ,  l ' , Effect ( , )Структурированная операционнаясемантикапосылкаНотацияозначает :следствие• если посылка истинная, то следствие такжеистинно;• это т.н.

правило вывода;• если посылка тождественно равна истине,то следствие – аксиома.Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеS  Loc  Eval (VP )«состояние: точка l + значение данных η»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеI   l , | l  Loc0 , ng0 «начальное состояние: начальная точка +все значения данных, удовлетворяющие g0»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеAP  Loc  Cond(VP )«высказывания вида: “в l” и “x∈D”, где D⊆dom(x);»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеL( l , )  {l}  g  Cond(VP ) | ng«состояние <l,η> размечается высказыванием “в l”и всеми высказываниями, истинными в η»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , где S  Act  S задано правиломg:l l ' n gl , l ' , Effect ( , )g:«Если l l ' и g истинно в η, тоl ,  l ' , Effect ( , ) »Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , где•••••S  Loc  Eval (VP ) S  Act  S задано правиломg:l l ' n gl , l ' , Effect ( , )I   l , | l  Loc0 , n g0 AP  Loc  Cond(VP )L( l , )  {l}  g  Cond (VP ) | ngПараллелизмЧередование (интерливинг)(напоминание)• Абстрагируемся от того, что система состоит измножества компонентов;• Действия независимых компонентов чередуются:– доступен один процессор, выполнение одного действияблокирует другие;• Порядок выполнения процессов неизвестен– Возможные порядки выполнения независимыхпроцессов P и Q:PPPQPQPQPQPPPPQQQPQPPQPPPQQ.

. .. . .. . .Чередование (интерливинг)• Обоснование чередования:эффект от параллельного выполнениянезависимых действий и равен эффектуот последовательного выполнения действийи в произвольном порядке;• Символьная запись:Effect ( |||  , )  Effect (( ;  )  (  ; ), )– « |||» – бинарный оператор чередования,– «;» – оператор последовательного выполнения,– «+» – оператор недетерминированного выбора.Чередование (интерливинг)x = x + 1 ||| y = y - 2αx=0α |||x=0y=7β y=5βαx = 0, y = 7βx = 1, y = 7x = 0, y = 5βαx = 1, y = 5Чередование систем переходов• Пусть TSi  Si , Acti , i , I i , APi , Li , i  1,2– две системы переходов• Система переходов TS1 |||TS2 определяется какS1  S2 , Act1  Act2 , , I1  I 2 , AP1  AP2 , L , где• L( s1 , s2 )  L1 ( s1 )  L2 ( s2 ) ,• отношение перехода  определяется правилами:s1 1 s1 's1 , s2 s1 ' , s2иs2 2 s2 's1 , s2 s1 , s2 'Чередование графов программ• Для графов программ PG1 (над V1) и PG2 (над V2) безразделяемых переменных (т.е.

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

Тип файла PDF

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

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

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