Лекция 1. Введение. Задача верификации аппаратуры и программного обеспечения (1185523), страница 4

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

Текст из файла (страница 4)

Rajamani, 2000)Èñòîðè÷åñêèå ñâåäåíèÿÌîäåëü âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãî âðåìåíè:âðåìåííûå àâòîìàòû(R. Alur, D.L. Dill, 1990)Èñòîðè÷åñêèå ñâåäåíèÿÌîäåëü âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãî âðåìåíè:âðåìåííûå àâòîìàòû(R. Alur, D.L. Dill, 1990)Àëãîðèòì âåðèôèêàöèè âðåìåííûõ àâòîìàòîâ(R. Alur, D.L. Dill, 1996)Èñòîðè÷åñêèå ñâåäåíèÿÌîäåëü âû÷èñëèòåëüíûõ ñèñòåì ðåàëüíîãî âðåìåíè:âðåìåííûå àâòîìàòû(R. Alur, D.L. Dill, 1990)Àëãîðèòì âåðèôèêàöèè âðåìåííûõ àâòîìàòîâ(R. Alur, D.L. Dill, 1996)Ñèñòåìà âåðèôèêàöèè UPPAAL(K. Larsen, 1995)Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàììÎäèí èç ïåðâûõ ïðèìåðîâ óñïåøíîãî ïðàêòè÷åñêîãîïðèìåíåíèÿ ôîðìàëüíûõ ìåòîäîâ âåðèôèêàöèè ïðîãðàììÿâëÿåòñÿ îáíàðóæåíèå â 1993 ã.

îøèáîê â ïðîòîêîëåêîãåððåíòíîñòè êåø-ïàìÿòè FutureBus+, êîòîðûé áûë ïðèíÿò âêà÷åñòâå IEEE ñòàíäàðòà è îïðåäåëÿåò àðõèòåêòóðó øèíû äëÿâûñîêîïðîèçâîäèòåëüíûõ êîìïüþòåðîâ. Ïðîâåðêà ïðàâèëüíîñòèïðîòîêîëà ïðîâîäèëàñü ïðè ïîìîùè ñèñòåìû âåðèôèêàöèèìîäåëåé ïðîãðàììì SMV.Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàììÄðóãèå ïðèìåðû óñïåøíîãî ïðèìåíåíèÿ ñðåäñòâ ôîðìàëüíîéâåðèôèêàöèè âêëþ÷àþò1. Ïðîåêò êîìïàíèè Immos Ltd (1988 ã.) ñîçäàíèÿìèêðîïðîöåññîðîâ äëÿ òðàíñïüþòåðîâ.ßçûê ñïåöèôèêàöèè Z.ßçûê ïðîãðàììèðîâàíèÿ Occam.Ìåòîä âåðèôèêàöèè äîêàçàòåëüñòâî ïðàâèëüíîñòè âëîãèêå Õîàðà.îáíàðóæåíû îøèáêè â ïðîöåäóðàõ îêðóãëåíèÿ èâû÷èñëåíèÿ îñòàòêîâ â áëîêå àðèôìåòèêè ñ ïëàâàþùåéòî÷êîé; ðàçðàáîòêà çàâåðøèëàñü íà 3 ìåñÿöà áûñòðåå, ÷åìó àëüòåðíàòèâíîé ãðóïïû ðàçðàáîò÷èêîâ, íåèñïîëüçîâàâøèõ ìåòîäû ôîðìàëüíîé âåðèôèêàöèè.Îêñôîðäñêèé óíèâåðñèòåò è Immos Ltd áûëè óäîñòîåíûQueen's Award for Technological Achievement.Ýôôåêò:Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì2.

Ïðîåêò êîìïàíèé GEC Alsthom, MATRA Transport, RATP(îïåðàòîð ïàðèæñêîãî îáùåñòâåííîãî òðàíñïîðòà) ïîêîìïüþòåðèçàöèè ñèñòåìû óïðàâëåíèÿ ïàðèæñêèì ìåòðî(RER) (1988 ã.).ßçûê ñïåöèôèêàöèè B.ßçûê ïðîãðàììèðîâàíèÿ Modula-2.Ìåòîä âåðèôèêàöèè äîêàçàòåëüñòâî ïðàâèëüíîñòè âëîãèêå Õîàðà.èñïîëüçîâàíèå ôîðìàëüíûõ ìåòîäîââåðèôèêàöèè ïîçâîëèëî èçáåæàòü òåñòèðîâàíèÿ îòäåëüíûõìîäóëåé ñèñòåìû è îãðàíè÷èòüñÿ ãëîáàëüíûìòåñòèðîâàíèåì. Âïîñëåäñòâèè ïî òîé æå ìåòîäèêåïðîâîäèëàñü ïîëíàÿ àâòîìàòèçàöèÿ îäíîé èç ëèíèéïàðèæñêîãî ìåòðî.Ýôôåêò:Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì3.

Ïðîåêò National Westminster Bank è êîìïàíèè PlatformSeven ïî ñîçäàíèþ ýëåêòðîííîé ïëàòåæíîé ñèñòåìû ñïðèìåíåíèåì smart-cards (8-áèòîâûé ìèêðîïðîöåññîð, 256áàéò RAM è íåñêîëüêî êèëîáàéò ROM) (1992 ã.).ßçûê ñïåöèôèêàöèè Z.Ìåòîä âåðèôèêàöèè äîêàçàòåëüñòâî (âðó÷íóþ) ñâîéñòâáåçîïàñíîñòè.îáíàðóæåíû è èñïðàâëåíû óÿçâèìîñòè; ïîëó÷åíîäîêàçàòåëüñòâî âûïîëíèìîñòè òðåáîâàíèé ñòàíäàðòàáåçîïàñíîñòè (200 ñòð.).Ýôôåêò:Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì4.

Ïðîåêò êîìïàíèè Airbus ïî àâòîìàòèçàöèè ïðîåêòèðîâàíèÿïðîãðàììíîãî îáåñïå÷åíèÿ è ýëåêòðîííîãî îáîðóäîâàíèÿäëÿ àâèàöèè è íàçåìíîãî òðàíñïîðòà (1982- íàñò. âðåìÿ ã.).ßçûê ñïåöèôèêàöèè Esterel.ßçûê ïðîãðàììèðîâàíèÿ Ñ, Verilog.Ìåòîä âåðèôèêàöèè model checking, àâòîìàòè÷åñêàÿãåíåðàöèÿ êîäà ïî ñïåöèôèêàöèÿì.ñîêðàùåíèå ÷èñëà îøèáîê â êîäå, 70% êîäàãåíåðèðóþòñÿ àâòîìàòè÷åñêè, ïîâûøåíèå îïåðàòèâíîñòèâíåñåíèÿ èçìåíåíèé â ïðîåêò.Ýôôåêò:Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì5. Ïðîåêò ñèñòåìû àâòîìàòè÷åñêîãî óïðàâëåíèÿ ïîäâèæíûìáàðüåðîì äëÿ çàùèòû Ðîòòåðäàìà îò íàâîäíåíèé (1992íàñò. âðåìÿ ã.).ßçûê ñïåöèôèêàöèè Z, Promela.ßçûê ïðîãðàììèðîâàíèÿ Ñ.Ìåòîä âåðèôèêàöèè model checking ñ èñïîëüçîâàíèåìñèñòåìû âåðèôèêàöèè SPIN.îáíàðóæåíèå îøèáîê â ñïåöèôèêàöèÿõ è êîäå.Ýôôåêò:Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì6.

Ïîëíàÿ âåðèôèêàöèÿ ìèêðîÿäðà linux (seL4) ãðóïïîéïðîãðàììèñòîâ èç ôèðìû ¾NICTA¿ (Àâñòðàëèÿ). (2009íàñò. âðåìÿ ã.).ßçûê ñïåöèôèêàöèè Hascel.ßçûê ïðîãðàììèðîâàíèÿ Ñ, AssemblerÌåòîä âåðèôèêàöèè Isabelle/HOL (èíòåðàêòèâíûé,ïîëóàâòîìàòè÷åñêèé ïðóâåð).Äîêàçàòåëüñòâî îòñóòñòâèÿ îøèáîêîïðåäåëåííîãî âèäà â êîäå ìèêðîÿäðà. "We can predictprecisely how the kernel will behave in every possiblesituation."Ýôôåêò:Äîñòèæåíèÿ ìåòîäîâ ôîðìàëüíîéâåðèôèêàöèè ïðîãðàìì 2003 ã.

À. Õîàð èíèöèèðîâàë ìåæäóíàðîäíûé ïðîåêòñîçäàíèÿ âåðèôèöèðóþùåãî êîìïèëÿòîðà êàê Grand Challengefor Computer Science.  2006 íà÷àòî ñîçäàíèå è ïîïîëíåíèåVeried Software Repository.Ïîäðàçäåëåíèÿ ôîðìàëüíûõ ìåòîäîâ âåðèôèêàöèè èìåþòñÿ âòàêèõ êîìïàíèÿõ êàê Microsoft, Intel, Cisco, IBM, Cadence,Synopsys, Mentor Graphics.Ïî îöåíêàì ýêñïåðòîâ çàäà÷àìè ðàçðàáîòêè è ïðèìåíåíèÿôîðìàëüíûõ ìåòîäîâ âåðèôèêàöèè â ìèðå çàíèìàþòñÿ ñâûøå4000 èññëåäîâàòåëåé.ÊÎÍÅÖ ËÅÊÖÈÈ 1..

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

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