Жүйелерді формалды тексеру әдістері

Кіріспе

Белгілі бір алгоритмдердің дұрыстығын дәлелдеу немесе жоққа шығару. Аппараттық және бағдарламалық жүйелер контекстінде, формальды тексеру – математиканың формальды әдістерін қолдана отырып, белгілі бір формальды сипаттамаға немесе қасиетке қатысты жүйенің дұрыстығын дәлелдеу немесе жоққа шығару амалы. Формальды тексеру жүйелерді формальды түрде сипаттауға ынталандыратын маңызды фактор және формальды әдістердің өзегі болып табылады. Ол электрондық жобалауды автоматтандырудағы талдау мен тексерудің маңызды аспектісі және бағдарламалық жасақтаманы тексерудің бір жолы. Формальды тексеруді қолдану компьютерлік қауіпсіздікті сертификаттаудың жалпы талаптары аясында бағалаудың ең жоғары деңгейін (EAL7) қамтамасыз етеді. Формальды тексеру мынадай жүйелердің дұрыстығын дәлелдеуге көмектеседі: криптографиялық протоколдар, комбинациялық тізбектер, ішкі жадысы бар цифрлық тізбектер және бағдарламалау тіліндегі бастапқы код түрінде жазылған бағдарламалық қамтамасыз ету. Тексерілген бағдарламалық жүйелердің көрнекті мысалдары – CompCert тексерілген C компиляторы және seL4 жоғары сенімділік операциялық жүйе ядросы. Бұл жүйелердің тексеруі жүйелердің математикалық моделіне формальды дәлелдің бар екенін қамтамасыз ету арқылы жүзеге асырылады. Жүйелерді модельдеу үшін қолданылатын математикалық объектілердің мысалдары: соны күйдегі автоматтары, белгіленген өту жүйелері, Хорн шарттары, Петри торлары, векторлық қосу жүйелері, уақытталған автоматтары, гибридтік автоматтары, процесс алгебрасы, бағдарламалау тілдерінің формальды семантикасы, мысалы, операциялық семантика, денотациялық семантика, аксиоматикалық семантика және Хоар логикасы.

Қадамдар

Бір тәсіл және қалыптасу – модельді тексеру, ол математикалық модельдің жүйелі түрде толық зерттелуінен тұрады (бұл шекті модельдер үшін мүмкін, сондай-ақ кейбір шексіз модельдер үшін де, онда шексіз күйлер жиынтығы абстракцияны пайдалану арқылы немесе симметриядан тиімді пайдалану арқылы шекті түрде бейнеленуі мүмкін). Әдетте, бұл модельдегі барлық күйлер мен өтулерді зерттеуден тұрады, осы үшін ақылды және салаға қатысты абстракция әдістерін қолдану арқылы бір операцияда күйлердің бүкіл топтарын қарастырып, есептеу уақытын қысқартуға болады. Іске асыру әдістеріне күй кеңістігін санау, символды күй кеңістігін санау, абстрактілі интерпретация, символды модельдеу, абстракцияны жетілдіру жатады. Тексерілетін қасиеттер көбінесе уақыт логикасында, мысалы, сызықтық уақыт логикасы (LTL), қасиеттерді сипаттау тілі (PSL), SystemVerilog Assertions (SVA) немесе есептеу ағашы логикасы (CTL) сияқты түрде сипатталады. Модельді тексерудің үлкен артықшылығы – ол көбінесе толық автоматты; оның негізгі кемшілігі – ол, әдетте, үлкен жүйелерге дейін кеңейтілмейді; символдық модельдер әдетте бірнеше жүз бит күймен шектеледі, ал нақты күйді санау зерттелген күй кеңістігінің салыстырмалы түрде кіші болуын қажет етеді. Тағы бір тәсіл – дедуктивті тексеру. Ол жүйеден және оның спецификацияларынан (немесе басқа да түсіндірмелерден) математикалық дәлелдеу міндеттемелерінің жиынтығын құрудан тұрады, олардың шындығы жүйенің спецификациясына сәйкес екенін көрсетеді, және осы міндеттемелерді дәлелдеуге көмектесетін құралдарды (интерактивті теорема дәлелдеушілерді) (мысалы, HOL, ACL2, Isabelle, Coq немесе PVS) немесе автоматты теорема дәлелдеушілерді, әсіресе, қанағаттандыру модулі теориялары (SMT) шешушілерді пайдалану арқылы орындаудан тұрады. Бұл тәсілдің кемшілігі – ол пайдаланушыдан жүйенің дұрыс жұмыс істеуінің себебін егжей-тегжейлі түсінуді және осы ақпаратты тексеру жүйесіне дәлелденуге тиісті теоремалардың тізбегі түрінде немесе жүйелік компоненттердің (мысалы, функциялар немесе процедуралар) және мүмкін, ішкі компоненттердің (мысалы, циклдар немесе деректер құрылымдары) спецификациялары (инварианттар, алғышарттар, постшарттар) түрінде жеткізуді талап етуі мүмкін.

One approach and formation is model checking, which consists of a systematically exhaustive exploration of the mathematical model (this is possible for finite models, but also for some infinite models where infinite sets of states can be effectively represented finitely by using abstraction or taking advantage of symmetry). Usually, this consists of exploring all states and transitions in the model, by using smart and domain specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, abstraction refinement. The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), or computational tree logic (CTL). The great advantage of model checking is that it is often fully automatic; its primary disadvantage is that it does not in general scale to large systems; symbolic models are typically limited to a few hundred bits of state, while explicit state enumeration requires the state space being explored to be relatively small. Another approach is deductive verification. It consists of generating from the system and its specifications (and possibly other annotations) a collection of mathematical proof obligations, the truth of which imply conformance of the system to its specification, and discharging these obligations using either proof assistants (interactive theorem provers) (such as HOL, ACL2, Isabelle, Coq or PVS), or automatic theorem provers, including in particular satisfiability modulo theories (SMT) solvers. This approach has the disadvantage that it may require the user to understand in detail why the system works correctly, and to convey this information to the verification system, either in the form of a sequence of theorems to be proved or in the form of specifications (invariants, preconditions, postconditions) of system components (e. g. functions or procedures) and perhaps subcomponents (such as loops or data structures).

Бағдарламалық жасақтама

Бағдарламалық бағдарламаларды ресми тексеру – бағдарламаның мінез-құлқының ресми сипаттамасына сәйкес келетінін дәлелдеуді қамтиды. Ресми тексерудің кіші салаларына дедуктивті тексеру (жоғарыда қараңыз), абстрактілі интерпретация, автоматтандырылған теоремаларды дәлелдеу, типтік жүйелер және жеңіл формалды әдістер жатады. Типке негізделген тексерудің перспективті тәсілі – тәуелді типті бағдарламалау, онда функциялардың типтері (кем дегенде бір бөлігі) сол функциялардың сипаттамаларын қамтиды, ал кодты типтік тексеру оның осы сипаттамаларға сәйкес дұрыстығын растайды. Толық мүмкіндіктермен жабдықталған тәуелді типтелген тілдер дедуктивті тексеруді ерекше жағдай ретінде қолдайды. Тағы бір толықтыратын тәсіл – бағдарлама туындылау, онда тиімді код функционалдық сипаттамалардан корректтілікті сақтайтын қадамдар сериясы арқылы жасалады. Бұл тәсілдің мысалы – Bird–Meertens формализмі, және оны құрылысы бойынша дұрыстықтың тағы бір түрі деп қарастыруға болады. Бұл әдістер дұрыс болуы мүмкін, яғни тексерілген қасиеттерді семантикадан логикалық тұрғыдан шығаруға болады, немесе дұрыс емес, яғни мұндай кепілдік жоқ. Дұрыс техника тек мүмкіндіктердің барлық кеңістігін қамтығаннан кейін ғана нәтиже береді. Дұрыс емес техниканың мысалы – мүмкіндіктердің тек бір бөлігін ғана қамтитын, мысалы, белгілі бір санға дейінгі бүтін сандарды ғана қамтитын және «жеткілікті жақсы» нәтиже беретін техника. Техникалар сондай-ақ шешілетін болуы мүмкін, яғни олардың алгоритмдік іске асырылуы жауаппен аяқталуы кепілдендірілген, немесе шешілмейтін, яғни олар ешқашан аяқталмауы мүмкін. Мүмкіндіктердің ауқымын шектеу арқылы, шешілетін дұрыс емес техникалар, шешілетін дұрыс техникалар болмаған жағдайда құрастырылуы мүмкін.

Тексеру және растау

Тексеру – өнімнің мақсатына сай келетіндігін сынаудың бір аспектісі. Валидация – осыған толықтыратын аспект. Көбінесе жалпы тексеру процесін V & V деп атайды.

Валидация: «Біз дұрыс нәрсе жасауға тырысып ба жатырмыз?», яғни өнім пайдаланушының нақты қажеттіліктеріне сәйкес берілген бе? Тексеру: «Біз жасағымыз келген нәрсені жасадық па?», яғни өнім талаптарға сай келе ме? Тексеру процесі статикалық/құрылымдық және динамикалық/мінез-құлық аспектілерінен тұрады. Мысалы, бағдарламалық өнім үшін бастапқы кодты (статикалық) қарап шығуға және нақты сынақ жағдайларымен (динамикалық) сынауға болады. Валидация көбінесе тек динамикалық түрде жүзеге асырылады, яғни өнімді әдеттегі және ерекше жағдайларда қолданып сынау арқылы тексеріледі («Барлық қолдану жағдайларын қанағаттандырады ма?» деген сұраққа жауап беріледі).

Бағдарламаны автоматты түрде жөндеу

Бағдарламаны жөндеу оракулға сәйкес жүзеге асырылады, оракул – бұл түзетілген нұсқаны тексеру үшін қолданылатын бағдарламаның қажетті функционалдығын қамтиды. Мысалы, тест жиынтығы – кіріс/шығыс жұптары бағдарламаның қызметін көрсетеді. Әртүрлі техникалар қолданылады, ең маңыздысы – қанағаттандыру теорияларымен (SMT) шешілетін мәселелерді қолдану және генетикалық бағдарламалау, эволюциялық есептеулерді түзетуге мүмкін үміткерлерді жасау және бағалау үшін пайдалану. Алғашқы әдіс детерминистік, ал екіншісі – кездейсоқ. Бағдарламаны жөндеу формалды тексеру және бағдарламаны синтездеу техникаларын біріктіреді. Формалды тексерудегі қателерді анықтау техникалары синтез модульдерімен жұмыс істейтін, мүмкін қате орналасқан бағдарламалық нүктелерді анықтау үшін қолданылады. Жөндеу жүйелері іздеу кеңістігін қысқарту үшін көбінесе белгілі бір, шешілген қателер класына назар аударады. Қазіргі техникалардың есептеу шығындарына байланысты өндірісте қолдану шектеулі.