Компьютерлік модельдерді тексеру әдісі

Кіріспе

Компьютерлік ғылым саласы
компьютерлік ғылымда модельдерді тексеру

Компьютерлік ғылымда модельді тексеру немесе қасиеттерді тексеру – жүйенің шекті күйдегі моделінің берілген сипаттамаға (сондай-ақ, дұрыстыққа) сәйкес келе ме екенін тексеру әдісі. Бұл көбінесе аппараттық немесе бағдарламалық жүйелермен байланысты, онда сипаттамада өміршеңдік талаптары (мысалы, тұйыққа тірелудің алдын алу) және қауіпсіздік талаптары (мысалы, жүйелік апатқа әкелетін күйлерді болдырмау) болады. Мұндай мәселені алгоритмдік түрде шешу үшін жүйенің моделі де, оның сипаттамасы да нақты математикалық тілде жазылады. Осы мақсатта, мәселе логикадағы міндет ретінде қойылады, атап айтқанда, құрылымның берілген логикалық формулаға сәйкес келе ме екенін тексеру үшін. Бұл жалпы ұғым логиканың көптеген түрлеріне және құрылымдардың көптеген түрлеріне қатысты. Ең қарапайым модельді тексеру мәселесі – берілген құрылымның ұсыныс логикасындағы формуламен сәйкес келе ме екенін тексеруден тұрады.

Шолу

Мүлікті тексеру екі сипаттама эквивалентті болмаған кезде растау үшін қолданылады. Нақтылау кезінде, спецификация жоғары деңгейдегі спецификацияда қажет емес егжей-тегжейлермен толықтырылады. Жаңа енгізілген қасиеттерді бастапқы спецификациямен салыстырудың қажеті жоқ, себебі мұндай салыстыру мүмкін емес. Сондықтан қатаң екі жақты эквиваленттілік тексеруі, бір жақты мүлікті тексеруге дейін жеңілдетіледі. Іске асыру немесе жобалау жүйенің моделі ретінде қарастырылады, ал спецификациялар – модельдің қанағаттандыруы тиіс қасиеттері. Аппараттық және бағдарламалық жасақтамалардың модельдерін тексеруге арналған модельді тексеру әдістерінің маңызды класы әзірленді, онда спецификация уақытша логикалық формуламен беріледі. Уақытша логиканы спецификациялау саласындағы пионерлік жұмысты Амир Пнуэли жасады, ол 1996 жылы «компьютерлік ғылымға уақытша логиканы енгізгені үшін» Тьюринг сыйлығын алды. Модельді тексеру Э.М. Кларк, Э.А. Эмерсон, Ж.П. Квейль және Ж. Сифакистің пионерлік жұмыстарымен басталды. Кларк, Эмерсон және Сифакис 2007 жылғы Тьюринг сыйлығын модельді тексеру саласын негіздеу және дамыту бойынша жасаған еңбектері үшін бөлісті. Модельді тексеру көбінесе аппараттық жобаларға қолданылады. Бағдарламалық жасақтама үшін, шешілмейтіндік (есептеу теориясына қараңыз) салдарынан, бұл тәсіл толық алгоритмдік бола алмайды, барлық жүйелерге қолданылмайды және әрқашан жауап бере алмайды; жалпы жағдайда, ол берілген қасиетті дәлелдеуге немесе жоққа шығаруға сәттілік таныта алмайды. Енгізілген жүйелердегі аппараттық құралдарда, спецификацияны, мысалы, UML белсенділік диаграммалары немесе басқарылатын Петри желілері арқылы растау мүмкін. Құрылым әдетте өндірістік аппараттық сипаттау тілінде немесе арнайы мақсаттағы тілде код түрінде беріледі. Мұндай бағдарлама – шекті күй машинасына (FSM) сәйкес келеді, яғни түйіндерден (немесе төбелерден) және қабырғалардан тұратын бағытталған граф. Әр түйінге атомдық мәлімдемелер жиынтығы сәйкес келеді, әдетте, қай жад элементтерінің бірге екенін көрсетеді. Түйіндер жүйенің күйін, ал қабырғалар күйді өзгерте алатын мүмкін болатын өтулерді білдіреді, ал атомдық мәлімдемелер – орындалу нүктесінде сақталатын негізгі қасиеттерді білдіреді. Формальды түрде, мәселе мынадай тұрғыда қойылуы мүмкін: берілген қасиет, уақытша логикалық формула түрінде берілген, және бастапқы күйі бар құрылым берілген болса, тура ма? Егер шекті болса, аппараттық құралдардағыдай, модельді тексеру графты іздеуге дейін тоғыстырылады.

Property checking is used for verification when two descriptions are not equivalent. During refinement, the specification is complemented with details that are unnecessary in the higher level specification. There is no need to verify the newly introduced properties against the original specification since this is not possible. Therefore, the strict bi directional equivalence check is relaxed to a one way property check. The implementation or design is regarded as a model of the system, whereas the specifications are properties that the model must satisfy. An important class of model checking methods has been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula. Pioneering work in temporal logic specification was done by Amir Pnueli, who received the 1996 Turing award for "seminal work introducing temporal logic into computing science". Model checking began with the pioneering work of E. M. Clarke, E. A. Emerson, by J. P. Queille, and J. Sifakis. Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their seminal work founding and developing the field of model checking. Model checking is most often applied to hardware designs. For software, because of undecidability (see computability theory) the approach cannot be fully algorithmic, apply to all systems, and always give an answer; in the general case, it may fail to prove or disprove a given property. In embedded systems hardware, it is possible to validate a specification delivered, e. g., by means of UML activity diagrams or control interpreted Petri nets. The structure is usually given as a source code description in an industrial hardware description language or a special purpose language. Such a program corresponds to a finite state machine (FSM), i. e., a directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node, typically stating which memory elements are one. The nodes represent states of a system, the edges represent possible transitions that may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution. Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula , and a structure with initial state , decide if If is finite, as it is in hardware, model checking reduces to a graph search.

Символды үлгілерді тексеру

Жетілетін күйлерді бірінен соң бірі тізімдеудің орнына, кейде күй кеңістігін бір қадамда көптеген күйлерді қарастыру арқылы тиімдірек шарлауға болады. Егер мұндай күй кеңістігін шарлау күйлер жиынтығы мен өту қатынастарын логикалық формулалар, екілік шешім диаграммалары (BDD) немесе басқа да байланысты деректер құрылымдары түрінде бейнелеуге негізделсе, модельді тексеру әдісі символдық болып саналады. Тарихи тұрғыдан алғанда, алғашқы символдық әдістер БДД-ны пайдаланды. 1996 жылы жасанды интеллекттегі жоспарлау мәселесін шешудегі ұсынысты қанағаттандырудың табысынан кейін (саттплан қараңыз), сол тәсіл сызықтық уақыт логикасы (LTL) үшін модельді тексеруге бейімделді: жоспарлау мәселесі қауіпсіздік қасиеттерін тексеруге сәйкес келеді. Бұл әдіс шектелген модельді тексеру деп аталады. Шектелген модельді тексерудегі Бульдік қанағаттандырушылық шешушілердің жетістігі символдық модельді тексеруде қанағаттандырушылық шешушілерді кеңінен қолдануға алып келді.

Техникалар

Модельді тексеру құралдары күй кеңістігінің комбинаторлық өсуімен, әдетте күйдің жарылу проблемасы деп аталатын құбылысқа тап болады, оны көптеген нақты әлемдегі проблемаларды шешу үшін қанағаттандыру қажет. Осы проблеманы жеңудің бірнеше тәсілі бар. Символикалық алгоритмдер шекті күй машиналарын (FSM) үшін графты тікелей құрудан аулақ болады; олардың орнына, олар графты сандық логикадағы формула арқылы жасырын түрде көрсетеді. Бинарлық шешім диаграммаларын (BDD) қолдануды Кен Макмиллан, сондай-ақ Оливье Кудерт және Жан Кристоф Мадре жұмыстары, CUDD және BuDDy сияқты ашық кодты BDD манипуляциялау кітапханаларын жасау арқасында танымал болды. Шектелген модельді тексеру алгоритмдері FSM-ді белгілі бір қадамдар санына дейін ашып, қасиет бұзушылығы осы қадамдардың ішінде немесе одан кемірек қадамда болатынын тексереді. Бұл әдетте шектеулі модельді SAT-тың бір мысалы ретінде кодтауды қамтиды. Бұл процесті барлық мүмкін бұзушылықтар жойылғанға дейін қайталауға болады (мысалы, итеративті тереңдеу іздеуі). Абстракция жүйенің қасиеттерін алдымен оны қарапайымдастыру арқылы дәлелдеуге тырысады. Қарапайымдастырылған жүйе әдетте түпнұсқа жүйемен бірдей қасиеттерге ие болмайды, сондықтан жетілдіру процесі қажет болуы мүмкін. Әдетте, абстракцияның дұрыс болуы талап етіледі (абстракцияда дәлелденген қасиеттер түпнұсқа жүйеге де қатысты); алайда, кейде абстракция толық болмайды (түпнұсқа жүйенің барлық дұрыс қасиеттері абстракцияға қатысты емес). Абстракцияның мысалы – бульдік емес айнымалылардың мәнін назарға алмау және тек бульдік айнымалылар мен бағдарламаның басқару ағынын қарастыру; мұндай абстракция, өрескел көрінсе де, мысалы, өзара қатыстылық қасиеттерін дәлелдеу үшін жеткілікті болуы мүмкін. Қарсы мысалмен басқарылатын абстракцияны жетілдіру (CEGAR) ірі (яғни, дәл емес) абстракциямен тексеруді бастайды және оны итеративті түрде жетілдіреді. Бұзушылық табылған кезде (яғни, қарсы мысал), құрал оның орындалу мүмкіндігін талдайды (яғни, бұзушылық шынайы ма, әлде толық емес абстракцияның салдары ма?). Егер бұзушылық орындалатын болса, ол пайдаланушыға хабарланады. Әйтпесе, орындалмау дәлелі абстракцияны жетілдіру үшін қолданылады және тексеру қайта басталады. Модельді тексеру құралдары бастапқыда дискретті күй жүйелерінің логикалық дұрыстығын анықтау үшін жасалған, бірақ содан бері олар нақты уақытты және гибридтік жүйелердің шектеулі формаларын қолдау үшін кеңейтілді.

Model checking tools face a combinatorial blow up of the state space, commonly known as the state explosion problem, that must be addressed to solve most real world problems. There are several approaches to combat this problem. Symbolic algorithms avoid ever explicitly constructing the graph for the finite state machines (FSM); instead, they represent the graph implicitly using a formula in quantified propositional logic. The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan, as well as of Olivier Coudert and Jean Christophe Madre, and the development of open source BDD manipulation libraries such as CUDD and BuDDy. Bounded model checking algorithms unroll the FSM for a fixed number of steps, , and check whether a property violation can occur in or fewer steps. This typically involves encoding the restricted model as an instance of SAT. The process can be repeated with larger and larger values of until all possible violations have been ruled out (cf. Iterative deepening depth first search). Abstraction attempts to prove properties of a system by first simplifying it. The simplified system usually does not satisfy exactly the same properties as the original one so that a process of refinement may be necessary. Generally, one requires the abstraction to be sound (the properties proved on the abstraction are true of the original system); however, sometimes the abstraction is not complete (not all true properties of the original system are true of the abstraction). An example of abstraction is to ignore the values of non boolean variables and to only consider boolean variables and the control flow of the program; such an abstraction, though it may appear coarse, may, in fact, be sufficient to prove e. g. properties of mutual exclusion. Counterexample guided abstraction refinement (CEGAR) begins checking with a coarse (i. e. imprecise) abstraction and iteratively refines it. When a violation (i. e. counterexample) is found, the tool analyzes it for feasibility (i. e., is the violation genuine or the result of an incomplete abstraction?). If the violation is feasible, it is reported to the user. If it is not, the proof of infeasibility is used to refine the abstraction and checking begins again. Model checking tools were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with real time and limited forms of hybrid systems.

Бірінші реттік логика

Модельді тексеру есептеу күрделілігі теориясы саласында да зерттеледі. Атап айтқанда, еркін айнымалылары жоқ бірінші реттік логикалық формула бекітіледі және келесі шешім есебі қарастырылады: берілген шекті интерпретация, мысалы, реляциялық деректер базасы ретінде сипатталған, интерпретация осы формуланың моделі бола ма, жоқ па, анықтаңыз. Бұл мәселе AC0 схемалар класына жатады. Кіріс құрылымына белгілі бір шектеулер қойғанда оны шешу мүмкін: мысалы, оның ағаш ені тұрақтымен шектелген болуы керек (бұл жалпы алғанда, монадты екінші реттік логика үшін модельді тексерудің шешілгіштігін білдіреді), әрбір домен элементінің дәрежесін шектеу және шектелген кеңею, жергілікті шектелген кеңею және ешқандай жерде тығыз емес құрылымдар сияқты жалпырақ жағдайлар. Бұл нәтижелер еркін айнымалылары бар бірінші реттік формуланың барлық шешімдерін санау міндетіне дейін кеңейтілді.