Ядро операционной системы Linux является крупнейшим проек-том с открытым исходным кодом. Исходный код модулей составляет большую часть исходного кода ядра.


Чтобы посмотреть этот PDF файл с форматированием и разметкой, скачайте его и откройте на своем компьютере.
Òåçèñûêîíôåðåíöèè¾Ëîìîíîñîâ2017¿
Ñòàòè÷åñêàÿâåðèôèêàöèÿìîäóëåéÿäðà
Linuxñó÷åòîììåæìîäóëüíûõñâÿçåé
ÏîëóøêèíÀëåêñåéÞðüåâè÷
Ñòóäåíò
ÔàêóëüòåòÂÌÊÌÃÓèìåíèÌ.Â.Ëîìîíîñîâà,Ìîñêâà,Ðîññèÿ
E-mail:
[email protected]
ßäðîîïåðàöèîííîéñèñòåìûLinuxÿâëÿåòñÿêðóïíåéøèìïðîåê-
òîìñîòêðûòûìèñõîäíûìêîäîì.Èñõîäíûéêîäìîäóëåéñîñòàâëÿåò
áîëüøóþ÷àñòüèñõîäíîãîêîäàÿäðà.Ìîäóëèäîëæíûîòâå÷àòüâû-
ñîêèìòðåáîâàíèÿìêíàäåæíîñòè,ïîñêîëüêóðàáîòàþòâòîìæåàä-
ðåñíîìïðîñòðàíñòâåèñòåìæåóðîâíåìïðèâèëåãèé,÷òîèîñòàëüíîå
ÿäðî[4].Îäíèìèçñïîñîáîâïðîâåðêèñîîòâåòñòâèÿêîäàïðîãðàììû
çàÿâëåííûìòðåáîâàíèÿìÿâëÿåòñÿñòàòè÷åñêàÿâåðèôèêàöèÿ.Èí-
ñòðóìåíòûñòàòè÷åñêîéâåðèôèêàöèèðåàëèçóþòòàêèåìåòîäû,êàê
BMC[2],CEGAR[3].
ÑèñòåìàKlever[5]ïðåäíàçíà÷åíàäëÿñòàòè÷åñêîéâåðèôèêàöèè
ìîäóëåéÿäðàLinuxïðèïîìîùèèíñòðóìåíòàñòàòè÷åñêîéâåðèôè-
êàöèèCPAchecker[1].ÏîñêîëüêóÿäðîÎÑLinuxÿâëÿåòñÿñëîæíûì
äëÿèíñòðóìåíòîâñòàòè÷åñêîéâåðèôèêàöèè,âñèñòåìåKleverèñ-
ïîëüçóåòñÿìîäåëèðîâàíèåîêðóæåíèÿ[6]äëÿîáåñïå÷åíèÿâîçìîæ-
íîñòèàíàëèçàèñõîäíîãîêîäàìîäóëÿîòäåëüíîîòèñõîäíîãîêîäà
îñòàëüíîãîÿäðà.Ìîäóëèìîãóòðåàëèçîâûâàòüèíòåðôåéñÿäðàèëè
ýêñïîðòèðóåìûåôóíêöèèäëÿèõèñïîëüçîâàíèÿâäðóãèõìîäóëÿõ.
ÌåòîäìîäåëèðîâàíèÿîêðóæåíèÿâñèñòåìåKleveríåïîçâîëÿåòâå-
ðèôèöèðîâàòüìîäóëèâûçûâàþùèåýêñïîðòèðóåìûåôóíêöèèâìå-
ñòåñèõðåàëèçàöèÿìè,âðåçóëüòàòå÷åãîâîçíèêàþòëîæíûåñîîáùå-
íèÿîáîøèáêàõ.Êðîìåòîãî,íåâåðèôèöèðóåòñÿêîäýêñïîðòèðóåìûõ
ôóíêöèé.
Äëÿñòàòè÷åñêîéâåðèôèêàöèèìîäóëåé,ðåàëèçóþùèõèëèâûçû-
âàþùèõýêñïîðòèðóåìûåôóíêöèè,ïðåäëàãàåòñÿìåòîäîáúåäèíåíèÿ
ìîäóëåéâãðóïïûäëÿñîâìåñòíîéñòàòè÷åñêîéâåðèôèêàöèè.Ìîäóëè
îáúåäèíÿþòñÿâãðóïïûâñîîòâåòñòâèèñîñâÿçÿìèïîýêñïîðòèðóå-
ìûìôóíêöèÿì.Ïîëüçîâàòåëüìîæåòíàñòðîèòüìàêñèìàëüíîå÷èñëî
ìîäóëåéâãðóïïå,âûáðàòüìîäóëü,âñåýêñïîðòèðóåìûåôóíêöèèêî-
òîðîãîäîëæíûáûòüïðîâåðèôèöèðîâàíû,èëèçàäàòüäðóãèåïàðà-
ìåòðû.Äëÿìîäåëèðîâàíèÿîêðóæåíèÿäëÿãðóïïûìîäóëåéïîòðå-
áîâàëîñüìîäèôèöèðîâàòüàëãîðèòìãåíåðàöèèìîäåëåéîêðóæåíèÿ,
÷òîáûðåàëèçîâàòüìîäåëèðîâàíèåçàãðóçêèèâûãðóçêèìîäóëåéèç
ïàìÿòè.
1
Òåêóùàÿñåêöèÿ
Ìåòîäáûëðåàëèçîâàíâñèñòåìåñòàòè÷åñêîéâåðèôèêàöèè
Klever.Äëÿàïðîáàöèèäàííîãîìåòîäàáûëîâûáðàíî66ìîäóëåé,êî-
òîðûåâåðèôèöèðîâàëèñüíàñîîòâåòñòâèå32òðåáîâàíèÿìêîððåêò-
íîñòè.Áûëîïîëó÷åíî3ëîæíûõñîîáùåíèÿîáîøèáêàõèç-çàîòñóò-
ñòâèÿèñõîäíîãîêîäàýêñïîðòèðóåìûõôóíêöèé.Ñîâìåñòíàÿâåðè-
ôèêàöèÿìîäóëåéïîçâîëèëàèçáàâèòüñÿîòñîîòâåòñòâóþùèõñîîá-
ùåíèéîáîøèáêàõèïîëó÷èòüêîððåêòíûéâåðäèêò.
Ëèòåðàòóðà
1.BeyerD.KeremogluM.E.CPACHECKER:atoolforcongurable
softwareverication//Proceedingsofthe23rdInternational
ConferenceonComputerAidedVerication,Berlin,Heidelberg,
2011,P.184190.
2.ClarkeE.BiereA.RaimiR.ZhuY.BoundedModelCheckingUsing

Приложенные файлы

  • pdf 7788056
    Размер файла: 112 kB Загрузок: 0

Добавить комментарий