Лекция 1. Введение. Задача верификации аппаратуры и программного обеспечения (1185523), страница 3
Текст из файла (страница 3)
Äîêàçàòåëüñòâî ïðàâèëüíîñòè îòäåëüíîãîïðîòîêîëà èëè ýëåêòðîííîé ñõåìû ìîæåò çàíÿòü öåëûå äíè èëèäàæå ìåñÿöû.Ïîýòîìó äåäóêòèâíûé àíàëèç èñïîëüçóåòñÿ ãëàâíûì îáðàçîìäëÿ ïðîâåðêè ñèñòåì, íàèáîëåå ÷óâñòâèòåëüíûõ ê ñáîÿì, êîãäàìîæíî âûäåëèòü íåîáõîäèìûå ðåñóðñû, äëÿ òîãî ÷òîáûãàðàíòèðîâàòü èõ áåçîïàñíîå èñïîëüçîâàíèå.Äåäóêòèâíûé àíàëèçÂàæíî îñîçíàâàòü òàêæå, ÷òî íå ñóùåñòâóåò àëãîðèòìà,ñïîñîáíîãî ðàñïîçíàòü, çàâåðøàåòñÿ ëè ðàáîòà ïðîèçâîëüíîéâû÷èñëèòåëüíîé ïðîãðàììû (íàïèñàííîé íà îäíîì èç ÿçûêîâïðîãðàììèðîâàíèÿ, íàïîäîáèå Cè èëè Ïàñêàëÿ). Ýòîîãðàíè÷èâàåò è âîçìîæíîñòè àâòîìàòè÷åñêîé âåðèôèêàöèè.
Â÷àñòíîñòè, ïðàâèëüíîñòü çàâåðøåíèÿ ðàáîòû ïðîãðàììû âîáùåì ñëó÷àå íåëüçÿ ïðîâåðèòü àâòîìàòè÷åñêè. Ïî ýòîéïðè÷èíå áîëüøèíñòâî ñèñòåì ïîñòðîåíèÿ äîêàçàòåëüñòâ íåìîãóò áûòü ïîëíîñòüþ àâòîìàòèçèðîâàíû.Ïðåèìóùåñòâî ìåòîäîâ äåäóêòèâíîãî àíàëèçà ñîñòîèò â òîì,÷òî îíè ìîãóò áûòü ïðèìåíåíû ê ñèñòåìàì ñ áåñêîíå÷íûì÷èñëîì ñîñòîÿíèé. Ýòó çàäà÷ó ìîæíî äî îïðåäåëåííûõïðåäåëîâ àâòîìàòèçèðîâàòü. Îäíàêî äàæå â òîì ñëó÷àå, êîãäàïðîâåðÿåìîå ñâîéñòâî äåéñòâèòåëüíî âûïîëíÿåòñÿ, íåëüçÿíàëîæèòü íèêàêèõ îãðàíè÷åíèé íà ïðîìåæóòîê âðåìåíè èîáúåì ïàìÿòè, íåîáõîäèìûé äëÿ ïîèñêà äîêàçàòåëüñòâà.Âåðèôèêàöèÿ ìîäåëåé ïðîãðàììÌåòîä âåðèôèêàöèè ìîäåëåé (èëè ïðîâåðêè âûïîëíèìîñòèñïåöèôèêàöèè íà ìîäåëè , èëè model checking ) ïðèìåíÿåòñÿäëÿ âåðèôèêàöèè ñèñòåì ñ êîíå÷íûì ÷èñëîì ñîñòîÿíèé.Îáû÷íî ïðîöåäóðà âåðèôèêàöèè çàêëþ÷àåòñÿ âèñ÷åðïûâàþùåì îáõîäå ïðîñòðàíñòâà ñîñòîÿíèé ñèñòåìû.
Ïðèíàëè÷èè äîñòàòî÷íûõ ðåñóðñîâ ýòà ïðîöåäóðà âñåãäàçàâåðøàåòñÿ è ìîæåò áûòü ðåàëèçîâàíà äîñòàòî÷íîýôôåêòèâíûì àëãîðèòìîì.Õîòÿ îãðàíè÷åíèå, ñâÿçàííîå ñ êîíå÷íûì ÷èñëîì ñîñòîÿíèéñèñòåìû, î÷åíü ñóùåñòâåííî, ìåòîä âåðèôèêàöèè ìîäåëåéïðèìåíèì êî ìíîãèì âàæíûì êëàññàì âû÷èñëèòåëüíûõ ñèñòåì:êîíòðîëëåðû, äðàéâåðû, êîììóíèêàöèîííûå ïðîòîêîëû. íåêîòîðûõ ñëó÷àÿõ ñèñòåìû ñ áåñêîíå÷íûì ÷èñëîìñîñòîÿíèé ìîãóò áûòü ïðîâåðåíû ýòèì ìåòîäîì â ñî÷åòàíèè ñðàçíîîáðàçíûìè ïðàâèëàìè àáñòðàêöèè è èíäóêöèè.Âåðèôèêàöèÿ ìîäåëåé ïðîãðàììÏîñêîëüêó ìåòîä ïðîâåðêè íà ìîäåëè ìîæåò ïðèìåíÿòüñÿ÷èñòî àâòîìàòè÷åñêè, îí ïðåäïî÷òèòåëüíåå äåäóêòèâíîãîàíàëèçà â òåõ ñëó÷àÿõ, êîãäà ìîæåò áûòü èñïîëüçîâàí.Òåì íå ìåíåå, âñåãäà îñòàíóòñÿ íåêîòîðûå æèçíåííî âàæíûåïðèëîæåíèÿ, äëÿ ïîëíîé âåðèôèêàöèè êîòîðûõ íåîáõîäèìîïðîâîäèòü äîêàçàòåëüñòâî òåîðåì. ñâÿçè ñ ýòèì ìîæíî îòìåòèòü íîâîå ïåðñïåêòèâíîåíàïðàâëåíèå, ïðåäóñìàòðèâàþùåå òàêóþ èíòåãðàöèþäåäóêòèâíîãî àíàëèçà è ìåòîäà ïðîâåðêè íà ìîäåëè, ÷òîáûôðàãìåíòû ñèñòåìû, èìåþùèå êîíå÷íîå ÷èñëî ñîñòîÿíèé,ïðîâåðÿëèñü àâòîìàòè÷åñêè.Ïðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÏðèíöèïû model checking1.
Äëÿ çàäàííîé âû÷èñëèòåëüíîé ñèñòåìû (ïðîãðàììû èëèïðîåêòà ìèêðîýëåêòðîííîé ñõåìû) ïîñòðîèòü ìîäåëü M äèñêðåòíóþ ñòðóêòóðó, êîòîðàÿÏðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÏðèíöèïû model checking1. Äëÿ çàäàííîé âû÷èñëèòåëüíîé ñèñòåìû (ïðîãðàììû èëèïðîåêòà ìèêðîýëåêòðîííîé ñõåìû) ïîñòðîèòü ìîäåëü M äèñêðåòíóþ ñòðóêòóðó, êîòîðàÿIìîæåò ðàññìàòðèâàòüñÿ êàê èíòåðïðåòàöèÿ äëÿ íåêîòîðîéôîðìàëüíîé ëîãèêè, èÏðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÏðèíöèïû model checking1. Äëÿ çàäàííîé âû÷èñëèòåëüíîé ñèñòåìû (ïðîãðàììû èëèïðîåêòà ìèêðîýëåêòðîííîé ñõåìû) ïîñòðîèòü ìîäåëü M äèñêðåòíóþ ñòðóêòóðó, êîòîðàÿIìîæåò ðàññìàòðèâàòüñÿ êàê èíòåðïðåòàöèÿ äëÿ íåêîòîðîéIîïèñûâàåò (íà íåêîòîðîì óðîâíå àáñòðàêöèè) ïîâåäåíèåôîðìàëüíîé ëîãèêè, èâû÷èñëèòåëüíîé ñèñòåìû.Ïðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÏðèíöèïû model checking1. Äëÿ çàäàííîé âû÷èñëèòåëüíîé ñèñòåìû (ïðîãðàììû èëèïðîåêòà ìèêðîýëåêòðîííîé ñõåìû) ïîñòðîèòü ìîäåëü M äèñêðåòíóþ ñòðóêòóðó, êîòîðàÿIìîæåò ðàññìàòðèâàòüñÿ êàê èíòåðïðåòàöèÿ äëÿ íåêîòîðîéIîïèñûâàåò (íà íåêîòîðîì óðîâíå àáñòðàêöèè) ïîâåäåíèåôîðìàëüíîé ëîãèêè, èâû÷èñëèòåëüíîé ñèñòåìû.2.
Äëÿ òåõíè÷åñêèõ òðåáîâàíèé, ïðåäúÿâëÿåìûõ ê ñèñòåìå,ñôîðìóëèðîâàòü ýòè òðåáîâàíèÿ íà ôîðìàëüíîìëîãè÷åñêîì ÿçûêå çàäàòü ñïåöèôèêàöèþ ϕ .Ïðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÏðèíöèïû model checking1. Äëÿ çàäàííîé âû÷èñëèòåëüíîé ñèñòåìû (ïðîãðàììû èëèïðîåêòà ìèêðîýëåêòðîííîé ñõåìû) ïîñòðîèòü ìîäåëü M äèñêðåòíóþ ñòðóêòóðó, êîòîðàÿIìîæåò ðàññìàòðèâàòüñÿ êàê èíòåðïðåòàöèÿ äëÿ íåêîòîðîéIîïèñûâàåò (íà íåêîòîðîì óðîâíå àáñòðàêöèè) ïîâåäåíèåôîðìàëüíîé ëîãèêè, èâû÷èñëèòåëüíîé ñèñòåìû.2. Äëÿ òåõíè÷åñêèõ òðåáîâàíèé, ïðåäúÿâëÿåìûõ ê ñèñòåìå,ñôîðìóëèðîâàòü ýòè òðåáîâàíèÿ íà ôîðìàëüíîìëîãè÷åñêîì ÿçûêå çàäàòü ñïåöèôèêàöèþ ϕ .3. Ïðîâåðèòü âûïîëíèìîñòü ñïåöèôèêàöèè ϕ íà ìîäåëè M :M |= ϕÏðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÏðèìåíåíèå ìåòîäà ïðîâåðêè âûïîëíèìîñòè ñïåöèôèêàöèè íàìîäåëè ñîñòîèò èç íåñêîëüêèõ ýòàïîâ.ÌîäåëèðîâàíèåÏåðâàÿ çàäà÷à çàêëþ÷àåòñÿ â ïðèâåäåíèè ïðîåêòèðóåìîéñèñòåìû ê òàêîìó ôîðìàëüíîìó âèäó, êîòîðûé áûë áûïðèåìëåì äëÿ èíñòðóìåíòàëüíûõ ñðåäñòâ âåðèôèêàöèèìîäåëåé ïðîãðàìì.×àñòî ýòî ïðîñòî çàäà÷à êîìïèëÿöèè.
 äðóãèõ ñëó÷àÿõ, ïðèîãðàíè÷åíèÿõ ïî âðåìåíè è îáúåìó ïàìÿòè, ìîäåëèðîâàíèåìîæåò ïîòðåáîâàòü àáñòðàêöèè, ÷òîáû èçáàâèòüñÿ îòíåñóùåñòâåííûõ äåòàëåé, íå îòíîñÿùèõñÿ ê äåëó.Ïðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÑïåöèôèêàöèÿÏåðåä ïðîâåäåíèåì âåðèôèêàöèè íóæíî ñôîðìóëèðîâàòüñâîéñòâà, êîòîðûìè äîëæíà îáëàäàòü ïðîåêòèðóåìàÿ ñèñòåìû.Îáû÷íî ñïåöèôèêàöèè çàäàþòñÿ íà ÿçûêå ôîðìàëüíîé ëîãèêè.Äëÿ àïïàðàòóðû è ïðîãðàììíîãî îáåñïå÷åíèÿ, êàê ïðàâèëî,ïðèìåíÿþò òåìïîðàëüíóþ ëîãèêó , ïîçâîëÿþùóþ îïèñûâàòü,êàê ïîâåäåíèå ñèñòåìû ïðîòåêàåò âî âðåìåíè.Âàæíûì âîïðîñîì ñïåöèôèêàöèè ÿâëÿåòñÿ ïîëíîòà . Ìåòîäïðîâåðêè íà ìîäåëè äàåò âîçìîæíîñòü óáåäèòüñÿ, ÷òî ìîäåëüïðîåêòèðóåìîé ñèñòåìû ñîîòâåòñòâóåò çàäàííîé ñïåöèôèêàöèè,îäíàêî îïðåäåëèòü, îõâàòûâàåò ëè çàäàííàÿ ñïåöèôèêàöèÿ âñåñâîéñòâà, êîòîðûìè äîëæíà îáëàäàòü ñèñòåìà, íåâîçìîæíî.Ïðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÂåðèôèêàöèÿ èäåàëüíîì ñëó÷àå âåðèôèêàöèÿ ïðîâîäèòñÿ ïîëíîñòüþàâòîìàòè÷åñêè.
Äëÿ ýòîãî èñïîëüçóþòñÿ ñòàíäàðòíûåàëãîðèòìû äèñêðåòíîé ìàòåìàòèêè, ê ÷èñëó êîòîðûõ îòíîñÿòñÿàëãîðèòìûI ïðîâåðêè âûïîëíèìîñòè áóëåâûõ ôîðìóë;I ïðîâåðêè äîñòèæèìîñòè çàäàííûõ âåðøèí â êîíå÷íîìãðàôå;I ïðîâåðêè äîñòèæèìîñòè ñèëüíî ñâÿçíûõ êîìïîíåíò âîðèåíòèðîâàííîì ãðàôå;I ïîñòðîåíèÿ ñõåì (äèàãðàìì), ðåàëèçóþùèõ áóëåâûôóíêöèè.Ïðîöåññ âåðèôèêàöèè ìîäåëåé ïðîãðàììÓòî÷íåíèå ìîäåëèÍà ïðàêòèêå âåðèôèêàöèÿ ÷àñòî òðåáóåò ñîäåéñòâèÿ ÷åëîâåêà.Îäíîé èç ñòîðîí äåÿòåëüíîñòè ÷åëîâåêà ÿâëÿåòñÿ àíàëèçðåçóëüòàòîâ âåðèôèêàöèè. Åñëè ðåçóëüòàòû ïðîâåðêèîòðèöàòåëüíûå, òî ïîëüçîâàòåëþ íåðåäêî ïðåäîñòàâëÿþòòðàññó, ñîäåðæàùóþ îøèáêó.
Îíà ñòðîèòñÿ â êà÷åñòâåêîíòðïðèìåðà äëÿ ïðîâåðÿåìîãî ñâîéñòâà è ìîæåò ïîìî÷üïðîåêòèðîâùèêó ïðîñëåäèòü, ãäå âîçíèêàåò îøèáêà.  ýòîìñëó÷àå àíàëèç îøèáî÷íîé òðàññû ìîæåò ïîâëå÷ü çà ñîáîéìîäèôèêàöèþ ñèñòåìû è ïîâòîðíîå ïðèìåíåíèå àëãîðèòìàïðîâåðêè íà ìîäåëè.Ñóùåñòâóþò ìåòîäû, êîòîðûå ïîçâîëÿþò àâòîìàòè÷åñêèóòî÷íÿòü ìîäåëü ïðîâåðÿåìîé ïðîãðàììû â òîì ñëó÷àå, êîãäàïðåäëîæåííûé êîíòðïðèìåð (òðàññà ïðåäïîëîæèòåëüíîîøèáî÷íîãî âû÷èñëåíèÿ) íå ðåàëèçóåòñÿ â ïðîãðàììå.Òåìïîðàëüíàÿ ëîãèêà è ìîäåëèÒåìïîðàëüíûå ëîãèêè ïîëåçíîå ñðåäñòâî ñïåöèôèêàöèèïàðàëëåëüíûõ ñèñòåì, ïîñêîëüêó îíè ïîçâîëÿþò îïèñûâàòüïîðÿäîê ñîáûòèé âî âðåìåíè áåç ïðèâëå÷åíèÿ ïàðàìåòðàâðåìåíè â ÿâíîì âèäå.Òåìïîðàëüíûå ëîãèêè îáû÷íî êëàññèôèöèðóþòñÿ âñîîòâåòñòâèè ñ òåì, ÿâëÿåòñÿ ëè ñòðóêòóðà âðåìåíèI ëèíåéíîé èëè âåòâÿùåéñÿ ;I äèñêðåòíîé èëè íåïðåðûâíîé .Cìûñë âñÿêîé ôîðìóëû òåìïîðàëüíîé ëîãèêè îïðåäåëÿåòñÿ ïîîòíîøåíèþ ê ðàçìå÷åííîìó ãðàôó ïåðåõîäîâ.
 ñèëó ïðè÷èíèñòîðè÷åñêîãî õàðàêòåðà ñòðóêòóðû òàêîãî âèäà íàçûâàþòñÿìîäåëÿìè Êðèïêå .Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Àêñèîìàòèçàöèÿ ìîäàëüíûõ ëîãèê (C.I. Lewis, 1910)Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Àêñèîìàòèçàöèÿ ìîäàëüíûõ ëîãèê (C.I. Lewis, 1910)Òåìïîðàëüíûå ëîãèêè (A.N. Prior, 1957)Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Àêñèîìàòèçàöèÿ ìîäàëüíûõ ëîãèê (C.I. Lewis, 1910)Òåìïîðàëüíûå ëîãèêè (A.N. Prior, 1957)Ñåìàíòèêà âîçìîæíûõ ìèðîâ (S. Kripke, 1959)Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Àêñèîìàòèçàöèÿ ìîäàëüíûõ ëîãèê (C.I. Lewis, 1910)Òåìïîðàëüíûå ëîãèêè (A.N. Prior, 1957)Ñåìàíòèêà âîçìîæíûõ ìèðîâ (S. Kripke, 1959)Ïðèìåíåíèå ìàòåìàòè÷åñêîé ëîãèêèäëÿ äîêàçàòåëüñòâà ïðàâèëüíîñòè ïðîãðàìì (C.A. Hoare, M.Floyd 1968)Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Àêñèîìàòèçàöèÿ ìîäàëüíûõ ëîãèê (C.I.
Lewis, 1910)Òåìïîðàëüíûå ëîãèêè (A.N. Prior, 1957)Ñåìàíòèêà âîçìîæíûõ ìèðîâ (S. Kripke, 1959)Ïðèìåíåíèå ìàòåìàòè÷åñêîé ëîãèêèäëÿ äîêàçàòåëüñòâà ïðàâèëüíîñòè ïðîãðàìì (C.A. Hoare, M.Floyd 1968)Äèíàìè÷åñêèå ëîãèêè (V. Pratt, 1976)Èñòîðè÷åñêèå ñâåäåíèÿÌîäàëüíûå ëîãèêè (Àðèñòîòåëü)Àêñèîìàòèçàöèÿ ìîäàëüíûõ ëîãèê (C.I.
Lewis, 1910)Òåìïîðàëüíûå ëîãèêè (A.N. Prior, 1957)Ñåìàíòèêà âîçìîæíûõ ìèðîâ (S. Kripke, 1959)Ïðèìåíåíèå ìàòåìàòè÷åñêîé ëîãèêèäëÿ äîêàçàòåëüñòâà ïðàâèëüíîñòè ïðîãðàìì (C.A. Hoare, M.Floyd 1968)Äèíàìè÷åñêèå ëîãèêè (V. Pratt, 1976)Ïðèìåíåíèå òåìïîðàëüíûõ ëîãèêäëÿ àíàëèçà ïàðàëëåëüíûõ ïðîãðàìì (A. Pnueli, 1977)Èñòîðè÷åñêèå ñâåäåíèÿÒàáëè÷íûé àëãîðèòì model checkingäëÿ òåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèé CTL(E.
Clarke, E. Emerson, J. Sifakis, 1981)Èñòîðè÷åñêèå ñâåäåíèÿÒàáëè÷íûé àëãîðèòì model checkingäëÿ òåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèé CTL(E. Clarke, E. Emerson, J. Sifakis, 1981)Ñâåäåíèå çàäà÷è model checking ê çàäà÷å ïðîâåðêå ïóñòîòûàâòîìàòîâ Áþõè(Systla A.P., Vardi M.Y., Wolper P., 1985)Èñòîðè÷åñêèå ñâåäåíèÿÒàáëè÷íûé àëãîðèòì model checkingäëÿ òåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèé CTL(E.
Clarke, E. Emerson, J. Sifakis, 1981)Ñâåäåíèå çàäà÷è model checking ê çàäà÷å ïðîâåðêå ïóñòîòûàâòîìàòîâ Áþõè(Systla A.P., Vardi M.Y., Wolper P., 1985)Ñèìâîëüíûé àëãîðèòì model checking,ñèñòåìà âåðèôèêàöèè SMV(K. McMillan, 1991)Èñòîðè÷åñêèå ñâåäåíèÿÒàáëè÷íûé àëãîðèòì model checkingäëÿ òåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèé CTL(E. Clarke, E. Emerson, J.
Sifakis, 1981)Ñâåäåíèå çàäà÷è model checking ê çàäà÷å ïðîâåðêå ïóñòîòûàâòîìàòîâ Áþõè(Systla A.P., Vardi M.Y., Wolper P., 1985)Ñèìâîëüíûé àëãîðèòì model checking,ñèñòåìà âåðèôèêàöèè SMV(K. McMillan, 1991)Ñèñòåìà âåðèôèêàöèè SPIN(Holzmann G.J., 1980-90)Èñòîðè÷åñêèå ñâåäåíèÿÒàáëè÷íûé àëãîðèòì model checkingäëÿ òåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèé CTL(E. Clarke, E. Emerson, J. Sifakis, 1981)Ñâåäåíèå çàäà÷è model checking ê çàäà÷å ïðîâåðêå ïóñòîòûàâòîìàòîâ Áþõè(Systla A.P., Vardi M.Y., Wolper P., 1985)Ñèìâîëüíûé àëãîðèòì model checking,ñèñòåìà âåðèôèêàöèè SMV(K. McMillan, 1991)Ñèñòåìà âåðèôèêàöèè SPIN(Holzmann G.J., 1980-90)Ñàìîíàñòðàèâàþùèéñÿ àëãîðèòì model checking,(Counter-example guided abstraction renement, CEGAR)Ñèñòåìû âåðèôèêàöèè Blast, Slam(T. Ball, S.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
