Лекция 3. Моделирование программ и схем

Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐÛ:Âëàäèìèð Àíàòîëüåâè÷ ÇàõàðîâÂëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâzakh@cs.msu.suËåêöèÿ 3.Ìîäåëèðîâàíèå ïðîãðàìì è ñõåìÂåðèôèêàöèÿ ìîäåëåé ïðîãðàììÎñíîâíûå ïðèíöèïûìîäåëèðîâàíèÿÌîäåëè ÊðèïêåÏðåäñòàâëåíèÿ ïåðâîãî ïîðÿäêàÑòåïåíü äåòàëèçàöèèïðåäñòàâëåíèÿÒðàíñëÿöèÿ ïðîãðàìì â ìîäåëèÊðèïêåÂåðèôèêàöèÿ ìîäåëåé ïðîãðàììÌåòîä âåðèôèêàöèè ìîäåëåé (èëè model checking )çàêëþ÷àåòñÿ â èñ÷åðïûâàþùåì îáõîäå ïðîñòðàíñòâà ñîñòîÿíèéñèñòåìû.

Ïðè íàëè÷èè äîñòàòî÷íûõ ðåñóðñîâ ýòà ïðîöåäóðàâñåãäà çàâåðøàåòñÿ è ìîæåò áûòü ðåàëèçîâàíà äîñòàòî÷íîýôôåêòèâíûì àëãîðèòìîì. íåêîòîðûõ ñëó÷àÿõ ñèñòåìû ñ áåñêîíå÷íûì ÷èñëîìñîñòîÿíèé ìîãóò áûòü ïðîâåðåíû ýòèì ìåòîäîì â ñî÷åòàíèè ñðàçíîîáðàçíûìè ïðàâèëàìè àáñòðàêöèè è èíäóêöèè.Ïîñêîëüêó ìåòîä ïðîâåðêè íà ìîäåëè ìîæåò ïðèìåíÿòüñÿ÷èñòî àâòîìàòè÷åñêè, îí ïðåäïî÷òèòåëüíåå äåäóêòèâíîãîàíàëèçà â òåõ ñëó÷àÿõ, êîãäà ìîæåò áûòü èñïîëüçîâàí.Âåðèôèêàöèÿ ìîäåëåé ïðîãðàììòðåáîâàíèÿïðàâèëüíîñòèïðîãðàììàèñïðàâëåíèå ïðîãðàììû(ñõåìà)Ôîðìàëèçàöèÿòðåáîâàíèé??ôîðìàëüíàÿñïåöèôèêàöèÿ? ??ôîðìàëüíàÿìîäåëüModelchecking? ?ÂÛÏÎËÍÅÍÎÌîäåëèðîâàíèå óòî÷íåíèå ìîäåëèñèñòåìûÑèìóëÿöèÿíå âûïîëíåíî,êîíòðïðèìåð 6Îøèáêèíåò@ ÎáíàðóæåíèåR@îøèáêè Âåðèôèêàöèÿ ìîäåëåé ïðîãðàììÐåçóëüòàò âåðèôèêàöèèìîäåëè ïðîãðàììíàñòîëüêî äîñòîâåðåí,íàñêîëüêî õîðîøî ïîñòðîåíàìîäåëü ïðîãðàììû.Ïëîõàÿ ìîäåëü áåñïîëåçíûå ðåçóëüòàòû.Ïðèíöèïû ìîäåëèðîâàíèÿ ñèñòåìÏåðâûì øàãîì ïðè ïðîâåðêå êîððåêòíîñòè ñèñòåìûÿâëÿåòñÿ îáñóæäåíèå è ñïåöèôèêàöèÿ ñâîéñòâ, êîòîðûìèîíà äîëæíà îáëàäàòü.Êàê òîëüêî ñòàíåò èçâåñòíî, êàêèå ñâîéñòâà ÿâëÿþòñÿâàæíûìè, ñëåäóþùèì øàãîì áóäåò ïîñòðîåíèåôîðìàëüíîé ìîäåëè ñèñòåìû.×òîáû ìîäåëü áûëà ïðèãîäíà äëÿ âåðèôèêàöèè, â íåéäîëæíû ïðîÿâëÿòüñÿ òå ñâîéñòâà, àíàëèç êîòîðûõíåîáõîäèì äëÿ óñòàíîâëåíèÿ åå êîððåêòíîñòè. òî æå âðåìÿ, îíà äîëæíà áûòü ñâîáîäíà îò ÷àñòíûõîñîáåííîñòåé, íå âëèÿþùèõ íà ïðîâåðÿåìûå ñâîéñòâà, íîóñëîæíÿþùèõ âåðèôèêàöèþ.Ïðèíöèïû ìîäåëèðîâàíèÿ ñèñòåìÍàïðèìåð, ïðè ìîäåëèðîâàíèè öèôðîâûõ ñõåìöåëåñîîáðàçíî ðàññóæäàòü â òåðìèíàõ ëîãè÷åñêèõ ÿ÷ååê èáóëåâûõ çíà÷åíèé, à íå â òåðìèíàõ óðîâíåé íàïðÿæåíèÿ.À ïðè èññëåäîâàíèè êîììóíèêàöèîííûõ ïðîòîêîëîâæåëàòåëüíî ñîñðåäîòî÷èòü âíèìàíèå íà îáìåíåñîîáùåíèÿìè, èãíîðèðóÿ ïðè ýòîì ñîäåðæàíèå ñàìèõñîîáùåíèé.Ïðèíöèïû ìîäåëèðîâàíèÿ ñèñòåìÏðè ïðîåêòèðîâàíèè ìèêðîýëåêòðîííîé àïïàðàòóðû èìåþòäåëî äåëî ñ ðåàãèðóþùèìè ñèñòåìàìè , ïîâåäåíèå êîòîðûõïðîÿâëÿåòñÿ âî âçàèìîäåéñòâèè ñ îêðóæàþùåé ñðåäîé.Ïåðâîé õàðàêòåðíîé ÷åðòîé ðåàãèðóþùåé ñèñòåìû ÿâëÿåòñÿ ååñîñòîÿíèå ¾ìîìåíòàëüíûé ñíèìîê¿ ñèñòåìû, â êîòîðîìçàïå÷àòëåíû çíà÷åíèÿ ïåðåìåííûõ â çàäàííûé ìîìåíòâðåìåíè.Íåîáõîäèìî òàêæå çíàòü, êàê èçìåíÿåòñÿ ñîñòîÿíèå ñèñòåìû âðåçóëüòàòå âûïîëíåíèÿ òåõ èëè èíûõ äåéñòâèé.

Ýòî èçìåíåíèåìîæíî îïèñàòü, óêàçàâ ñîñòîÿíèå ñèñòåìû äî âûïîëíåíèÿäåéñòâèÿ è åå ñîñòîÿíèå ïîñëå âûïîëíåíèÿ äåéñòâèÿ. Òàêàÿïàðà ñîñòîÿíèé îïðåäåëÿåò ïåðåõîä ñèñòåìû.Âû÷èñëåíèå ðåàãèðóþùåé ñèñòåìû îïðåäåëÿåòñÿ â òåðìèíàõïåðåõîäîâ ñèñòåìû. Âû÷èñëåíèå ýòî áåñêîíå÷íàÿïîñëåäîâàòåëüíîñòü ñîñòîÿíèé, êàæäîå èç êîòîðûõ ïîëó÷åíî èçïðåäûäóùåãî ïîñðåäñòâîì íåêîòîðîãî ïåðåõîäà.Ïðèíöèïû ìîäåëèðîâàíèÿ ñèñòåìÄëÿ ôîðìàëèçàöèè íàøèõ ïðåäñòàâëåíèé î ïîâåäåíèèðåàãèðóþùèõ ñèñòåì ìû âîñïîëüçóåìñÿ ðàçíîâèäíîñòüþðàçìå÷åííîãî ãðàôà ïåðåõîäîâ, êîòîðàÿ íàçûâàåòñÿìîäåëüþ Êðèïêå .Ìîäåëü Êðèïêå ñîñòîèò èç ìíîæåñòâà ñîñòîÿíèé,ìíîæåñòâà ïåðåõîäîâ ìåæäó ñîñòîÿíèÿìè è ôóíêöèè,êîòîðàÿ ïîìå÷àåò êàæäîå ñîñòîÿíèå íàáîðîì ñâîéñòâ,èñòèííûõ â ýòîì ñîñòîÿíèè.

Ïóòè â ìîäåëè Êðèïêåñîîòâåòñòâóþò âû÷èñëåíèÿì ñèñòåìû.Ìîäåëè ÊðèïêåÐàññìîòðèì ìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèé AP .Ìîäåëüþ Êðèïêå M íàä ìíîæåñòâîì àòîìàðíûõ âûñêàçûâàíèéAP íàçîâåì ÷åòâåðêó M = (S, S0 , R, L) , â êîòîðîé:1) S êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé ;2) S0 ⊆ S ìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé ;3) R ⊆ S × S îòíîøåíèå ïåðåõîäîâ , êîòîðîå îáÿçàíî áûòüòîòàëüíûì, ò.

å. äëÿ êàæäîãî ñîñòîÿíèÿ s ∈ S äîëæíîñóùåñòâîâàòü òàêîå ñîñòîÿíèå s 0 ∈ S , ÷òî èìååò ìåñòîR(s, s 0 ) ;4) L : S → 2AP ôóíêöèÿ ðàçìåòêè , êîòîðàÿ ïîìå÷àåòêàæäîå ñîñòîÿíèå ìíîæåñòâîì àòîìàðíûõ âûñêàçûâàíèé,èñòèííûõ â ýòîì ñîñòîÿíèè.Ìîäåëè ÊðèïêåÏóòü â ìîäåëè M èç ñîñòîÿíèÿ s0 ýòî òàêàÿ áåñêîíå÷íàÿïîñëåäîâàòåëüíîñòü ñîñòîÿíèé π = s0 , s1 , s2 , . . .

, ÷òî s0 = s èäëÿ âñåõ i > 0 âûïîëíÿåòñÿ R(si , si+1 ) .Ñîñòîÿíèå s íàçûâàåòñÿ äîñòèæèìûì ñîñòîÿíèåì ìîäåëè, åñëè÷åðåç s ïðîõîäèò ïóòü, âåäóùèé èç êàêîãî-ëèáî íà÷àëüíîãîñîñòîÿíèÿ ìîäåëè.Ñîñòîÿíèå s íàçûâàåòñÿ òóïèêîâûì ñîñòîÿíèåì ìîäåëè, åñëèëþáîé ïóòü èç s ïðîõîäèò ïðîõîäèò òîëüêî ÷åðåç ñîñòîÿíèå s(îáðàçóåò ïåòëþ).Èíîãäà ïåðåõîäû ìîäåëè Êðèïêå ïîìå÷àþòñÿ èìåíàìè òåõäåéñòâèé ïðîãðàììû, êîòîðûå ñîîòâåòñòâóþò ýòèì ïåðåõîäàì. ýòîì ñëó÷àå ââîäèòñÿ ìíîæåñòâî äåéñòâèé Act è îòíîøåíèåïåðåõîäîâ çàäàåòñÿ òðîéêàìè R ⊆ S × Act × S .Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ëîäî÷íèê ìîæåò ïåðåïðàâèòüñÿ ÷åðåç ðåêóîäèíÌîäåëü Êðèïêå: Ïåðåïðàâà.Ëîäî÷íèê ìîæåò ïåðåïðàâèòüñÿ ÷åðåç ðåêóîäèíÌîäåëü Êðèïêå: Ïåðåïðàâà.èëè ñ ïàññàæèðîìÌîäåëü Êðèïêå: Ïåðåïðàâà.èëè ñ ïàññàæèðîìÌîäåëü Êðèïêå: Ïåðåïðàâà.Áåç ïðèñìîòðà ëîäî÷íèêàíåêîòîðûå ïàññàæèðû ìîãóò ïîñòðàäàòüÌîäåëü Êðèïêå: Ïåðåïðàâà.Áåç ïðèñìîòðà ëîäî÷íèêàíåêîòîðûå ïàññàæèðû ìîãóò ïîñòðàäàòüÌîäåëü Êðèïêå: Ïåðåïðàâà.×òî íàì âàæíî çíàòü?Âàæíî çíàòüæèâ ïåðñîíàæ èëè íåò,ãäå íàõîäèòñÿ ïåðñîíàæ.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìíîæåñòâî ñîñòîÿíèé ìîäåëè Êðèïêå ÏåðåïðàâàS = {−1, 0, 1}4 .Äëÿ êàæäîãî ñîñòîÿíèÿ (x1 , x2 , x3 , x4 )xi = −1 îçíà÷àåò, ÷òî ïåðñîíàæ i íàõîäèòñÿ íà ëåâîì áåðåãó,xi = 1 îçíà÷àåò, ÷òî ïåðñîíàæ i íàõîäèòñÿ íà ïðàâîì áåðåãó,xi = 0 îçíà÷àåò, ÷òî ïåðñîíàæà i óæå íå ñóùåñòâóåò.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ìíîæåñòâî ñîñòîÿíèé ìîäåëè Êðèïêå ÏåðåïðàâàS = {−1, 0, 1}4 .Äëÿ êàæäîãî ñîñòîÿíèÿ (x1 , x2 , x3 , x4 )xi = −1 îçíà÷àåò, ÷òî ïåðñîíàæ i íàõîäèòñÿ íà ëåâîì áåðåãó,xi = 1 îçíà÷àåò, ÷òî ïåðñîíàæ i íàõîäèòñÿ íà ïðàâîì áåðåãó,xi = 0 îçíà÷àåò, ÷òî ïåðñîíàæà i óæå íå ñóùåñòâóåò.Ìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèéS0 = {(−1, −1, −1, −1)}Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :(-1,-1,-1,-1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :(-1,-1,-1,1))(-1,-1,-1,-1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :(-1,-1,-1,1))(1,-1,-1,1)(-1,-1,-1,-1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :(-1,-1,-1,1))(-1,-1,-1,-1)@@@(1,-1,-1,1)R@(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :(-1,-1,-1,1))(-1,-1,-1,-1)P@@PPPP@(1,-1,-1,1)R@(-1,1,-1,1)PPq(-1,-1,1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,0,-1,1)(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,0,-1,1)?(-1,-1,0,1)(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,0,-1,1)?(-1,-1,0,1)(-1,0,0,1)(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,0,-1,1)?(-1,-1,0,1)@@@(-1,0,0,1)R@(-1,-1,0,-1)(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,0,-1,1)??(-1,-1,0,1)(1,-1,0,1)@@@(-1,0,0,1)R@(-1,-1,0,-1)(-1,1,-1,1)Ìîäåëü Êðèïêå: Ïåðåïðàâà.Îòíîøåíèå ïåðåõîäîâ R :1(-1,-1,-1,-1)PPPP@PP@)qP(-1,-1,-1,1)(-1,-1,1,1)@R@(1,-1,-1,1)(-1,1,-1,1)(-1,0,-1,1)??(-1,-1,0,1)(1,-1,0,1)@@@(-1,0,0,1)R@?(-1,-1,0,-1)è.ò.ä.Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ðàññìîòðèì ìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèéAP = {alivei , lefti : i = 1, 2, 3, 4}Ôóíêöèÿ ðàçìåòêè L :Ìîäåëü Êðèïêå: Ïåðåïðàâà.Ðàññìîòðèì ìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèéAP = {alivei , lefti : i = 1, 2, 3, 4}Ôóíêöèÿ ðàçìåòêè L :L((−1, −1, −1, −1)) = AP ,L((−1, 0, 1, 1)) = {alive1 , alive3 , alive4 , left1 },è.ò.ä.Ïðèíöèïû ìîäåëèðîâàíèÿ ñèñòåìÑóùåñòâóþò ðàçëè÷íûå òèïû ïàðàëëåëüíûõ ñèñòåì(ñèíõðîííûå è àñèíõðîííûå ñõåìû, ïðîãðàììû ñðàçäåëÿåìûìè ïåðåìåííûìè, ïðîãðàììû,âçàèìîäåéñòâóþùèå ïóòåì îáìåíà ñîîáùåíèÿìè, è ò.

ä.).Ââèäó òàêîãî ðàçíîîáðàçèÿ, íóæåí óíèâåðñàëüíûéôîðìàëèçì, â ðàìêàõ êîòîðîãî ìîæíî áûëî áûïðåäñòàâëÿòü ïàðàëëåëüíóþ ñèñòåìó ëþáîãî òèïà.Äëÿ ýòîãî ïðèãîäíû ôîðìóëû ëîãèêè ïðåäèêàòîâ ïåðâîãîïîðÿäêà. Ïî ôîðìóëå, ïðåäñòàâëÿþùåé ïàðàëëåëüíóþñèñòåìó, ñòðîèòñÿ ìîäåëü Êðèïêå, àäåêâàòíîñîîòâåòñòâóþùàÿ ýòîé ñèñòåìå.Ïðåäñòàâëåíèÿ ïåðâîãî ïîðÿäêàÄëÿ îïèñàíèÿ ïàðàëëåëüíûõ ñèñòåì ïðèãîäíû ôîðìóëûïåðâîãî ïîðÿäêà, èìåþùèå ôèêñèðîâàííóþ èíòåðïðåòàöèþ.Ýòî îçíà÷àåò, ÷òî ïðåäèêàòíûå è ôóíêöèîíàëüíûå ñèìâîëû,âñòðå÷àþùèåñÿ â òàêèõ ôîðìóëàõ, áóäóò èìåòüïðåäîïðåäåëåííîå çíà÷åíèå.Ðàññìîòðèì ìíîæåñòâî V = {v1 , .