Лекция 1. Введение. Задача верификации аппаратуры и программного обеспечения
Описание файла
PDF-файл из архива "Лекция 1. Введение. Задача верификации аппаратуры и программного обеспечения", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Ìàòåìàòè÷åñêèåìåòîäûâåðèôèêàöèèïðîãðàìì è ñõåìËÅÊÒÎÐÛ:Âëàäèìèð Àíàòîëüåâè÷ Çàõàðîâ,Âëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâ6 ñåíòÿáðÿ 2016 ã.ÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ1. Ââåäåíèå. Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ1. Ââåäåíèå. Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿ2. Äåäóêòèâíûé ìåòîä âåðèôèêàöèè ïðîãðàììÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ1. Ââåäåíèå. Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿ2. Äåäóêòèâíûé ìåòîä âåðèôèêàöèè ïðîãðàìì3. Äèñêðåòíûå ìîäåëè ïàðàëëåëüíûõ ïðîãðàìì èñõåìÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ1.
Ââåäåíèå. Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿ2. Äåäóêòèâíûé ìåòîä âåðèôèêàöèè ïðîãðàìì3. Äèñêðåòíûå ìîäåëè ïàðàëëåëüíûõ ïðîãðàìì èñõåì4. Òåìïîðàëüíûå ëîãèêèÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ1. Ââåäåíèå. Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿ2. Äåäóêòèâíûé ìåòîä âåðèôèêàöèè ïðîãðàìì3. Äèñêðåòíûå ìîäåëè ïàðàëëåëüíûõ ïðîãðàìì èñõåì4. Òåìïîðàëüíûå ëîãèêè5. Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì äëÿòåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèéCTL: òàáëè÷íûé è ñèìâîëüíûé ïîäõîäÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ1. Ââåäåíèå. Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿ2. Äåäóêòèâíûé ìåòîä âåðèôèêàöèè ïðîãðàìì3.
Äèñêðåòíûå ìîäåëè ïàðàëëåëüíûõ ïðîãðàìì èñõåì4. Òåìïîðàëüíûå ëîãèêè5. Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì äëÿòåìïîðàëüíîé ëîãèêè äåðåâüåâ âû÷èñëåíèéCTL: òàáëè÷íûé è ñèìâîëüíûé ïîäõîä6. Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì äëÿòåìïîðàëüíîé ëîãèêè ëèíåéíîãî âðåìåíè LTL:òåîðåòèêî-àâòîìàòíûé ïîäõîäÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ7. Ìåòîäû ïîâûøåíèÿ ýôôåêòèâíîñòèâåðèôèêàöèè: àáñòðàêöèÿ, ñèìóëÿöèÿ,ðåäóêöèÿ ÷àñòè÷íûõ ïîðÿäêîâ, îãðàíè÷åííàÿâåðèôèêàöèÿÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ7.
Ìåòîäû ïîâûøåíèÿ ýôôåêòèâíîñòèâåðèôèêàöèè: àáñòðàêöèÿ, ñèìóëÿöèÿ,ðåäóêöèÿ ÷àñòè÷íûõ ïîðÿäêîâ, îãðàíè÷åííàÿâåðèôèêàöèÿ8. Ìîäåëè âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãîâðåìåíèÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ7. Ìåòîäû ïîâûøåíèÿ ýôôåêòèâíîñòèâåðèôèêàöèè: àáñòðàêöèÿ, ñèìóëÿöèÿ,ðåäóêöèÿ ÷àñòè÷íûõ ïîðÿäêîâ, îãðàíè÷åííàÿâåðèôèêàöèÿ8. Ìîäåëè âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãîâðåìåíè9. Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì ðåàëüíîãîâðåìåíèÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ7.
Ìåòîäû ïîâûøåíèÿ ýôôåêòèâíîñòèâåðèôèêàöèè: àáñòðàêöèÿ, ñèìóëÿöèÿ,ðåäóêöèÿ ÷àñòè÷íûõ ïîðÿäêîâ, îãðàíè÷åííàÿâåðèôèêàöèÿ8. Ìîäåëè âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãîâðåìåíè9. Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì ðåàëüíîãîâðåìåíè10. Ìåòîäû ñòàòè÷åñêîãî àíàëèçà ìîäåëåéïðîãðàììÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀ7. Ìåòîäû ïîâûøåíèÿ ýôôåêòèâíîñòèâåðèôèêàöèè: àáñòðàêöèÿ, ñèìóëÿöèÿ,ðåäóêöèÿ ÷àñòè÷íûõ ïîðÿäêîâ, îãðàíè÷åííàÿâåðèôèêàöèÿ8.
Ìîäåëè âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãîâðåìåíè9. Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì ðåàëüíîãîâðåìåíè10. Ìåòîäû ñòàòè÷åñêîãî àíàëèçà ìîäåëåéïðîãðàìì11. Ìåòîäû óòî÷íåíèÿ àáñòðàêöèé ïîêîíòðïðèìåðàìÏÐÎÃÐÀÌÌÀ ÊÓÐÑÀÊîíñïåêòû ëåêöèé áóäóò ðàçìåùàòüñÿ ïîàäðåñóhttp://mk.cs.msu.ruËèòåðàòóðàIIIIÝ.Ì.
Êëàðê, Î. Ãðàìáåðã, Ä. Ïåëåä. Âåðèôèêàöèÿ ìîäåëåéïðîãðàìì: Model Checking. Èçä-âî ÌÖÍÌÎ, 2002.Þ.Ã. Êàðïîâ. Model Checking: âåðèôèêàöèÿ ïàðàëëåëüíûõè ðàñïðåäåëåííûõ ïðîãðàììíûõ ñèñòåì. Èçä-âîÁÕÂ-Ïåòåðáóðã, 2010.K. R. Apt, E.-R. Olderog. Verication of sequential andconcurrent programs, Springer, 1997.B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L.Petrucci, P. Schnoebelen. Systems and Software Verication:Model-Checking Techniques and Tools.
Springer, 2001.I Baier C., Katoen J.-P. Principles of model checking,MIT Press, 2008.Ëåêöèÿ 1.Çàäà÷à âåðèôèêàöèè àïïàðàòóðû èïðîãðàììíîãî îáåñïå÷åíèÿ1. Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?2. Îñíîâíûå ïîäõîäû ê çàäà÷å ôîðìàëüíîéâåðèôèêàöèè.3. Ïðèíöèïû âåðèôèêàöèè ìîäåëåé ïðîãðàìì.4. Èñòîðè÷åñêèå ñâåäåíèÿ.5. Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?Çàäà÷ó ñïåöèôèêàöèè è âåðèôèêàöèè ïðîãðàìì è ïðîåêòíûõðåøåíèé ìèêðîýëåêòðîííîé àïïàðàòóðû äîëãîå âðåìÿ áûëîïðèíÿòî ðàññìàòðèâàòü êàê íåêîòîðóþ âñïîìîãàòåëüíóþäåÿòåëüíîñòü, êàê ñâîåîáðàçíûé íåèçáåæíûé ¾äîâåñîê¿ êîñíîâíîìó çàíÿòèþ ïðîãðàììèñòà ðàçðàáîòêà è ðåàëèçàöèÿïðîãðàììíîãî êîäà.Îäíàêî â íà÷àëå 80-õ ãîäîâ ïðîøëîãî âåêà ðàçðàáîò÷èêèïðîãðàììíîãî îáåñïå÷åíèÿ îáíàðóæèëè, ÷òî ñâûøå ïîëîâèíûèçäåðæåê, ñâÿçàííûõ ñ èçãîòîâëåíèå ïðîãðàììíîãî ïðîäóêòàèëè ìèêðîñõåìû, ïðèõîäÿòñÿ èìåííî íà ýòàï âåðèôèêàöèè, èýòà äîëÿ íåóêëîííî âîçðàñòàåò.Ñðåäè íàèáîëåå çíà÷èìûõ ïðè÷èí, îáúÿñíÿþùèõ ýòî ÿâëåíèå,ìîæíî âûäåëèòü ñëåäóþùèå.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1.
Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììåÀïïàðàòíûå è ïðîãðàììíûå ñèñòåìû øèðîêî èñïîëüçóåòñÿ âîìíîãèõ ïðèëîæåíèÿõ, ãäå ëþáîé îòêàç ñ÷èòàåòñÿíåäîïóñòèìûì, òàêèõ êàêI ýíåðãåòèêà,I ýëåêòðîííàÿ êîììåðöèÿ,I òåëåêîììóíèêàöèÿ,I ñèñòåìû óïðàâëåíèÿ âîçäóøíûì è äîðîæíûì äâèæåíèåì,I ìåäèöèíñêàÿ àïïàðàòóðà,è ñïèñîê ýòîò äîâîëüíî âåëèê.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1.
Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììå22 èþëÿ 1962 ã. ïåðâàÿ ñòóïåíü ðàêåòû Ìàðèíåð-1 áûëàâçîðâàíà ÷åðåç 293 ñåêóíäû ïîñëå ñòàðòà. Àíòåííà àïïàðàòàïîòåðÿëà ñâÿçü ñ íàâîäÿùåé ñèñòåìîé íà Çåìëå, â ðåçóëüòàòåóïðàâëåíèå âçÿë íà ñåáÿ áîðòîâîé êîìïüþòåð, ïðîãðàììàêîòîðîãî ñîäåðæàëà îøèáêó.
 îò÷åòå ÍÀÑÀ, îòïðàâëåííîì âÊîíãðåññ â 1963, óïîìèíàåòñÿ: ¾Ïðîïóñê äåôèñà âðåäàêòèðîâàíèè äàííûõ âûíóäèë êîìïüþòåð äàòü ñåðèþíåíóæíûõ ñèãíàëîâ î êîððåêöèè êóðñà, êîòîðûå ñáèëè êîðàáëüñ êóðñà è ïðèâåëè ê åãî óíè÷òîæåíèþ.¿Ñïóñòÿ íåñêîëüêî ëåò Àðòóð Êëàðê ïèñàë, ÷òî Ìàðèíåð-1 áûë¾óíè÷òîæåí ñàìûì äîðîãèì äåôèñîì â èñòîðèè¿.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1.
Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììå4 èþíÿ 1996 ã. åâðîïåéñêàÿ êîñìè÷åñêàÿ ðàêåòà ¾Àðèàí-5¿âçîðâàëàñü ìåíåå ÷åì ÷åðåç ñîðîê ñåêóíä ïîñëå çàïóñêà.Ïðè÷èíîé ïîñëóæèëà îøèáêà â ïðîãðàììå êîìïüþòåðà,îòâå÷àâøåãî çà ðàñ÷åòû äâèæåíèÿ ðàêåòû.  õîäå çàïóñêàâîçíèêëà èñêëþ÷èòåëüíàÿ ñèòóàöèÿ, êîãäà áîëüøîå64-ðàçðÿäíîå ÷èñëî ñ ïëàâàþùåé òî÷êîé áûëî ïðåîáðàçîâàíî â16-ðàçðÿäíîå öåëîå ÷èñëî.
Ýòî ïðåîáðàçîâàíèå íå áûëîçàùèùåíî êîäîì äëÿ îáðàáîòêè èñêëþ÷èòåëüíûõ ñèòóàöèé, ÷òîè ïðèâåëî ê ñáîþ êîìïüþòåðà. Òà æå ñàìàÿ îøèáêà ïðèâåëà êñáîþ äóáëèðóþùåãî êîìïüþòåðà.  ðåçóëüòàòå íà áîðòîâîéêîìïüþòåð ðàêåòû áûëè ïåðåäàíû íåâåðíûå äàííûå î âûñîòå,÷òî âûçâàëî óíè÷òîæåíèå ðàêåòû.Ñòîèìîñòü óùåðáà 370 000 000 $.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1. Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììå 1999 ã. Îäèí èç ñóáïîäðÿä÷èêîâ NASA ïîñòàâèëïðîãðàììíîå îáåñïå÷åíèå â êîòîðîì èñïîëüçîâàëàñüàíãëèéñêàÿ ñèñòåìà ìåð, â òî âðåìÿ êàê èçìåðèòåëüíîåîáîðóäîâàíèå áûëî îòêàëèáðîâàíî ïî ìåòðè÷åñêîé ñèñòåìå.Ýòî ïîñëóæèëî ïðè÷èíîé àâàðèè ñïóòíèêà, îòïðàâëåííîãî íàÌàðñ.
Ñòîèìîñòü óùåðáà ñîñòàâèëà 327 000 000 $.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1. Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììåÌåäèöèíñêèé àïïàðàò ðàäèàöèîííîé òåðàïèè Therac-25 ïåðèîä1985-87 ãã. ïîäàâàë íåêîòîðûì ïàöèåíòàì äîçû îáëó÷àíèÿ,ïðåâûøàþùèå ïðåäïèñàííûå âðà÷àìè â 100 ðàç. Áûëîîáíàðóæåíî, ÷òî ïðè÷èíîé ïîñëóæèëà îøèáêà â ïðîãðàììíîìîáåñïå÷åíèè, óïðàâëÿþùèì àïïàðàòîì. Ïðåâûøåíèå äîçûîáëó÷åíèÿ ïîñëóæèëî íåïîñðåäñòâåííîé ïðè÷èíîé ñìåðòè ïîêðàéíåé òðåõ ïàöèåíòîâ.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1. Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììåÌåäèöèíñêèé àïïàðàò ðàäèàöèîííîé òåðàïèè Therac-25 ïåðèîä1985-87 ãã. ïîäàâàë íåêîòîðûì ïàöèåíòàì äîçû îáëó÷àíèÿ,ïðåâûøàþùèå ïðåäïèñàííûå âðà÷àìè â 100 ðàç.
Áûëîîáíàðóæåíî, ÷òî ïðè÷èíîé ïîñëóæèëà îøèáêà â ïðîãðàììíîìîáåñïå÷åíèè, óïðàâëÿþùèì àïïàðàòîì. Ïðåâûøåíèå äîçûîáëó÷åíèÿ ïîñëóæèëî íåïîñðåäñòâåííîé ïðè÷èíîé ñìåðòè ïîêðàéíåé òðåõ ïàöèåíòîâ. 2000 ã. â Ïàíàìå íåñêîëüêî ïàöèåíòîâ ïîëó÷èëèïåðåäîçèðîâêó îáëó÷åíèÿ ïðè ðàäèîòåðàïèè. Áûëî îáíàðóæåíî,÷òî óïðàâëÿþùàÿ ïðîãðàììà çàäàâàëà ìîùíîñòü èçëó÷åíèÿ âçàâèñèìîñòè îò ïîðÿäêà, â êîòîðîì ïîñòóïàëè íåêîòîðûåäàííûå ïî ïàðàëëëåëüíûì êàíàëàì (ýôôåêò ¾ãîíîê¿).Ïåðåäîçèðîâêà ïîñëóæèëà ïðè÷èíîé ñìåðòè ïî ìåíüøåé ìåðåïÿòè ïàöèåíòîâ.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1. Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììåÏðîãðàììíîå îáåñïå÷åíèå ñèñòåìû óïðàâëåíèÿïðîòâîâîçäóøíîãî ðàêåòíîãî êîìïëåêñà MIM-104 Patriotñîäåðæàëà îøèáêó, â ñèëó êîòîðîé òàéìåðû â ðàçíûõêîìïüþòåðàõ â ñîñòàâå ýòîãî êîìïëåêñà èìåëè òåíäåíöèþ êðàññèíõðîíèçàöèè 0.3 ñåê íà 100 ÷àñîâ íåïðåðûâíîé ðàáîòû.
Âðåçóëüòàòå 25 ôåâðàëÿ 1991 ã. òàêîé êîìïëåêñ íå ñìîãîñóùåñòâèòü ïåðåõâàò èðàêñêîé òàêòè÷åñêîé ðàêåòû, ÷òîïðèâåëî ê ãèáåëè 28 âîåííîñëóæàùèõ àðìèè ÑØÀ.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1. Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììå 1998 ã.
â ÑØÀ íà ïîëãîäà áûë çàäåðæàí ââîä â ñòðîé íîâîéñèñòåìû îáñëóæèâàíèÿ àâèàöèîííîãî òðàíñïîðòà èç-çàíåïðåêðàùàþùèõñÿ ñáîåâ â ðàáîòå ïðîãðàììíîãî îáåñïå÷åíèÿýòîé ñèñòåìû. Ïî îöåíêàì ýêñïåðòîâ óùåðá ñîñòàâèë íåñêîëüêîñîòåí ìèëëèîíîâ äîëëàðîâ.Knight Capital Group ïîòåðÿëà 440 000 000 $ çà 45 ìèíóò âðåçóëüòàòå íåêîððåêòíîé óñòàíîâêè îáíîâëåííîé âåðñèèïðîãðàììíîãî îáåñïå÷åíèÿ íà ñåðâåðû, èç-çà ÷åãî â òå÷åíèåíåêîòîðîãî âðåìåíè ïðîèñõîäèëà ïîïåðåìåííàÿ ðàáîòà ñòàðîãîè íîâîãî êîäà.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?1. Âîçðàñòàíèå ñòîèìîñòè óùåðáà èç-çàïðîïóùåííîé îøèáêè â ïðîãðàììåCòàòèñòè÷åñêèå èññëåäîâàíèÿ ïîêàçûâàþò, ÷òî ñâûøå 10%ïðîåêòîâ ïî ðàçðàáîòêå ìèêðîýëåêòðîííûõ ñõåì òàê è íåäîâîäÿòñÿ äî ñåðèéíîãî èçãîòîâëåíèÿ, ââèäó ñóùåñòâåííûõîøèáîê, êîòîðûå îáíàðóæèâàþòñÿ â õîäå ýêñïëàóòàöèèîïûòíûõ îáðàçöîâ.
Còîèìîñòü ðàçðàáîòêè ñõåìû èèçãîòîâëåíèÿ åå îïûòíîãî îáðàçöà ìîæåò ñîñòàâëÿòü íåñêîëüêîñîòåí òûñÿ÷ äîëëàðîâ.Èññëåäîâàíèÿ, ïðîâåäåííûå â 2002 ã. ÍàöèîíàëüíûìÈíñòèòóòîì Ñòàíäàðòîâ è Òåõíîëîãèé, ïîêàçàëè, ÷òî ïîòåðèýêîíîìèêè èç-çà îøèáîê â ïðîãðàììíîì îáåñïå÷åíèÿîöåíèâàþòñÿ ñóììîé 59.5 ìèëëèàðäîâ äîëëàðîâ, ïðè÷åì ýòîòóùåðá ìîæíî ñîêðàòèòü íà òðåòü çà ñ÷åò óñîâåðøåíñòâîâàíèÿìåòîäîâ âåðèôèêàöèè ïðîãðàìì.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?2. Ðàñøèðåíèå îáëàñòè ïðèìåíåíèÿ ïðîãðàììíîãîîáåñïå÷åíèÿÏî ìåðå òîãî êàê âîçðàñòàåò ó÷àñòèå ïðîãðàììíûõ ñèñòåì âíàøåé æèçíè, ðàñòåò è áðåìÿ îòâåòñòâåííîñòè çà ïðàâèëüíîñòüèõ ôóíêöèîíèðîâàíèÿ. Áåçîïàñíîñòü óæå íåëüçÿ âîññòàíîâèòü,ïðîñòî îòêëþ÷èâ íåïðàâèëüíî ðàáîòàþùóþ ñèñòåìó:îòêëþ÷åíèå óñòðîéñòâà íåñåò áîëüøóþ îïàñíîñòü.Ìû ñòàíîâèìñÿ çàâèñèìûìè îò ïðàâèëüíîñòèôóíêöèîíèðîâàíèÿ âû÷èñëèòåëüíûõ óñòðîéñòâ.
Ïîýòîìó åùåáîëåå íàñóùíîé çàäà÷åé ñòàíîâèòñÿ ðàçðàáîòêà ìåòîäîâ,ñïîñîáñòâóþùèõ ïîâûøåíèþ íàøåé óâåðåííîñòè âïðàâèëüíîñòè ðàáîòû ïîäîáíûõ ñèñòåì. Èçìåíÿåòñÿ ñàìîïîíèìàíèå çàäà÷è âåðèôèêàöèè: ïðîãðàììà ìîæåò áûòüïðèçíàíà íàäåæíîé íå ïîòîìó, ÷òî â íåé íå óäàëîñüîáíàðóæèòü îøèáîê, à ïîòîìó, ÷òî óäàëîñü óáåäèòåëüíîäîêàçàòü îòñóòñòâèå îøèáîê.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?3.