lect05 (К. Савенков - Верификация программ на моделях (2010))

Верификация программна моделяхЛекция №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) безразделяемых переменных (т.е.