Жұмыс істеп тұрған жүйенің верификациясы: қасиеттерді бақылау және талдау

Кіріспе

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

Мысалдар

Төмендегі мысалдарда бірнеше орындау уақытында тексеру топтары осы мәтін жазылған кезде (2011 жылдың сәуірінде) қарастырылған бірнеше қарапайым қасиеттер талқыланады. Оларды қызықтырақ ету үшін төмендегі әрбір қасиет әртүрлі спецификация формализмін қолданады және барлығы да параметрлік. Параметриялық қасиеттер – параметрлік оқиғалармен құрылған іздер туралы қасиеттер, бұл оқиғалар деректерді параметрлермен байланыстырады. Мұнда параметрлік қасиет мына түрде келеді: , мұнда – бұл жалпы (көшірмеленбеген) параметрлік оқиғаларға сілтеме жасайтын тиісті формализмдегі спецификация. Мұндай параметрлік қасиеттердің мәні – қасиеттің өзі байқалатын ізде кездесетін барлық параметрлік мәндер үшін орындалуы керек. Келесі мысалдардың ешқайсысы нақты бір орындау уақытында тексеру жүйесіне тән емес, бірақ параметрлерді қолдау міндетті. Келесі мысалдарда Java синтаксисі қолданылады, сондықтан "==" логикалық теңдік, ал "=" – тағайындау. Кейбір әдістер (мысалы, UnsafeEnumExample-дағы жаңарту) – Java API-нің бөлігі емес, түсініктілік үшін қолданылатын фиктивті әдістер.

Келесі

Java Iterator интерфейсі hasNext әдісін шақыруды және келесі әдіс шақырылғанға дейін true мәнін қайтаруды талап етеді. Егер бұл орындалмаса, пайдаланушы Коллекцияның соңына дейін итерация жасауы мүмкін. Оң жақтағы суретте осы қасиетті тексеру және күшпен орындау үшін қолданылатын, мүмкін мониторды анықтайтын шекті күй машинасы көрсетілген. Белгісіз күйден келесі әдісті шақыру қате болады, себебі мұндай операция қауіпсіз болмауы мүмкін. Егер hasNext шақырылып, true мәнін қайтарса, next әдісін шақыру қауіпсіз, сондықтан монитор more күйіне өтеді. Егер hasNext әдісі false мәнін қайтарса, онда элементтердің саны таусылған, және монитор none күйіне өтеді. More және none күйлерінде hasNext әдісін шақыру жаңа ақпарат бермейді. More күйінен next әдісін шақыру қауіпсіз, бірақ тағы элементтер бар-жоқ екені белгісіз болады, сондықтан монитор бастапқы белгісіз күйіне қайта оралады. Соңында, none күйінен next әдісін шақыру қате күйіне түсуге әкеледі. Келесі бөлімде осы қасиеттің параметрлік өткен уақыттың сызықтық уақыт логикасы арқылы көрсетілуі келтірілген. Бұл формула next әдісін шақырудың алдында hasNext әдісі шақырылып, true мәнін қайтаруы керек екенін көрсетеді. Бұл қасиет Iterator i үшін параметрлік. Тұжырымдамалық тұрғыдан алғанда, бұл сынақ бағдарламасындағы әрбір мүмкін Iterator үшін монитордың бір данасы болады дегенді білдіреді, бірақ орындау уақытын тексеру жүйелері өздерінің параметрлік мониторларын осылай жүзеге асыруға міндетті емес. Бұл қасиеттің мониторы формула бұзылған кезде (яғни, шекті күй машинасы қате күйіне өткенде) оқиғаны басқарушыны іске қосу үшін орнатылады. Бұл немесе next әдісі hasNext әдісін шақырмастан шақырылғанда, немесе hasNext әдісі next әдісінен бұрын шақырылып, false мәнін қайтарғанда болады.

Қауіпсіз

Java-дағы Vector класының элементтерін итерациялаудың екі тәсілі бар. Бұрынғы мысалда көрсетілгендей, Iterator интерфейсін немесе Enumeration интерфейсін пайдалануға болады. Iterator интерфейсі үшін жою әдісін қосудан басқа, басты айырмашылық – Iterator «fail-fast» қағидасын қолданады, ал Enumeration қолданбайды. Бұл, егер Iterator интерфейсін пайдаланып Vector-ды итерациялау кезінде (Iterator-дың жою әдісін қолданбастан) өзгертуге тырыссаңыз, ConcurrentModificationException қатесі туындайды дегенді білдіреді. Дегенмен, Enumeration қолданғанда мұндай қате туындамайды, жоғарыда айтылғандай. Бұл бағдарламадан белгісіз нәтижелерге әкелуі мүмкін, себебі Enumeration тұрғысынан қарағанда Vector тұрақсыз күйде қалады. Enumeration интерфейсін әлі де қолданатын ескі бағдарламалар үшін, олардың негізгі Vector-ы өзгерген кезде Enumeration-дар қолданылмауына көз жеткізу қажет. Осы мінез-құлықты қамтамасыз ету үшін келесі параметрлік реттегіш үлгі қолданылуы мүмкін:

∀ Vector v, Enumeration e: (e = v.elements) (e.nextElement)* v.update e.nextElement

Бұл үлгі Enumeration және Vector екеуі үшін де параметрлік. Интуитивті түрде, және жоғарыда көрсетілгендей, орындалу уақытын тексеру жүйелері өздерінің параметрлік мониторларын осылай іске асыруға міндетті емес, бұл қасиет үшін параметрлік мониторды Vector мен Enumeration-ның әрбір мүмкін жұбы үшін параметрлік емес монитордың экземплярын құру және бақылау деп түсінуге болады. Кейбір оқиғалар бірнеше мониторларға қатысты болуы мүмкін, мысалы v.update, сондықтан орындалу уақытын тексеру жүйесі оларды (қайтадан концептуалды түрде) барлық мүдделі мониторларға жіберуі керек. Мұнда қасиет бағдарламаның қате мінез-құлығын көрсетеді. Осы қасиетті үлгіге сәйкес келетінін бақылау қажет. Оң жақтағы суретте осы үлгіге сәйкес келетін Java коды көрсетілген, осылайша ол қасиетті бұзады. Vector, v, Enumeration, e құрылғаннан кейін жаңартылады, содан кейін e қолданылады.

Қауіпсіз бұғаттау

Алдыңғы екі мысал шекті күй қасиеттерін көрсетеді, бірақ орындалу уақытында тексеруде қолданылатын қасиеттер әлдеқайда күрделі болуы мүмкін. SafeLock қасиеті берілген әдіс шақыруында (қайта кіретін) Lock класының алу және босату санының сәйкес келуін қамтамасыз етеді. Бұл, әрине, оларды алу әдістерінен басқа әдістерде құлыптарды босатуға жол бермейді, бірақ бұл сыналған жүйенің қол жеткізе алатын қажетті мақсат болуы мүмкін. Төменде осы қасиеттің параметрлік контекстсіз үлгі арқылы берілген сипаттамасы келтірілген:

∀ Сызып t, Құлып l: S→ε | S бастау(t) S аяқтау(t) | S l. алу(t) S l. босату(t)

Үлгі әр Сызып және Құлып үшін тіркескен бастау/аяқтау және алу/босату жұптарының теңгерімді тізбектерін көрсетеді (бос тізбек). Мұнда бастау және аяқтау бағдарламадағы әрбір әдістің басталуы мен аяқталуын білдіреді (алу және босату шақыруларын қоспағанда). Олар Сызыпқа қатысты параметрлік, себебі әдістердің басталуы мен аяқталуы бір Сызыпқа жататын болса ғана байланыстырылуы керек. Алу және босату оқиғалары да осы себепті Сызыпқа қатысты параметрлік болып табылады. Олар, сонымен қатар, Құлыпқа қатысты параметрлік, өйткені біз бір Құлыптың босатуларын екіншісінің алуларымен байланыстырғымыз келмейді. Ең экстремалды жағдайда, Сызып пен Құлыптың әр мүмкін комбинациясы үшін қасиеттің бір данасы, яғни контекстсіз талдау механизмінің көшірмесі болуы мүмкін; бұл қайтадан интуитивті, себебі орындалу уақытын тексеру жүйелері бірдей функционалдылықты әртүрлі жолдармен іске асыруы мүмкін. Мысалы, егер жүйеде Сызыптар , , және мен Құлыптар және болса, онда <,>, <,>, <,>, <,>, <,>, және <,> жұптары үшін қасиеттің инстанцияларын сақтау қажет болуы мүмкін. Бұл қасиеттің үлгіге сәйкес келмеушіліктеріне қадағалау жүргізу қажет, себебі үлгі дұрыс мінез-құлықты көрсетеді. Оң жақтағы сурет осы қасиетті екі рет бұзатын ізді көрсетеді. Суреттегі төмен қарайтын қадамдар әдістің басталуын, ал жоғары қарайтын қадамдар – аяқталуын білдіреді. Суреттегі сұр жебелер бір Құлыптың берілген алулары мен босатулары арасындағы сәйкестікті көрсетеді. Қарапайымдылық үшін, ізде тек бір Сызып және бір Құлып көрсетілген.

Ғылыми-зерттеу салалары мен қолдануы

Іске қосылу кезіндегі тексеру саласындағы зерттеулердің көп бөлігі төменде тізілген тақырыптардың біріне немесе бірнешеуіне қатысты.

Жүгіру уақытын қысқарту

Орындалатын жүйені бақылау әдетте кейбір орындалу уақытында қосымша шығынға (аппараттық мониторлар ерекше жағдайларды құрайды) әкеледі. Реттеу уақытында тексеру құралдарының қосымша шығынын барынша азайту маңызды, әсіресе құрылған мониторлар жүйемен бірге қолданылғанда. Орындалу уақытындағы қосымша шығынды азайту тәсілдері:

Жақсартылған құралдар. Орындалатын жүйеден оқиғаларды алу және оларды мониторларға жіберу, дұрыс жабдықталмаған жағдайда үлкен қосымша шығынға әкелуі мүмкін. Кез келген реттеу уақытында тексеру құралы үшін жақсы жүйелік құралдар маңызды, егер құрал қолданыстағы орындалу журналдарын мақсат етпесе. Қазіргі кезде көптеген құралдық тәсілдер бар, олардың әрқайсысының артықшылықтары мен кемшіліктері бар, жеке немесе қолмен жасалған құралдардан бастап, мамандандырылған кітапханаларға дейін, аспектіге бағытталған тілдерге компиляцияға дейін, виртуалды машинаны кеңейтуге дейін, аппараттық қолдауды пайдалануға дейін. Статикалық талдаумен үйлестіру. Статикалық және динамикалық талдаудың кең таралған үйлесімі, әсіресе компиляторларда кездеседі, статикалық түрде растала алмайтын барлық талаптарды бақылау болып табылады. Реттеу уақытында тексеруде бұл тәсіл кеңінен қолданылады, атап айтқанда, статикалық талдауды қолдану арқылы толыққанды бақылау көлемін азайту. Статикалық талдау бақылауға алынатын қасиеттерге де, бақылауға алынатын жүйеге де қолданылуы мүмкін. Бақыланатын қасиеттің статикалық талдауы кейбір оқиғаларды бақылаудың қажетсіз екенін, кейбір мониторларды құруды кейінге қалдыруға болатындығын және кейбір қолданыстағы мониторлар ешқашан іске қосылмайтынын, сондықтан оларды қоқыс жинауға болатындығын көрсетеді. Бақыланатын жүйенің статикалық талдауы мониторларға ешқашан әсер етпейтін кодты анықтай алады. Мысалы, жоғарыдағы HasNext қасиетін бақылау кезінде, i.next шақыруының алдындағы i.hasnext шақыруы true мәнін қайтаратын кез келген жолдағы кодты құралмен жабдықтаудың қажеті жоқ (бақылау ағыны графигінде көрінеді). Тиімді монитор құру және басқару. Жоғарыдағы мысалдардағыдай параметрлік қасиеттерді бақылау кезінде, бақылау жүйесі әрбір параметрлік мысалға қатысты бақыланатын қасиеттің күйін қадағалап отыруы керек. Мұндай мысалдардың саны теориялық тұрғыдан шексіз, ал тәжірибеде өте көп. Зерттеудің маңызды мәселесі - байқалған оқиғаларды оларды қажет ететін мысалдарға қалай тиімді жіберу. Осыған байланысты қиындықтар: мұндай мысалдардың санын қалайша азайту (жіберу жылдамдығын арттыру үшін), яғни, қажетсіз мысалдарды жасаудан мүмкіндігінше аулақ болу және, керісінше, қажетсіз болған кезде бұрын жасалған мысалдарды қалайша жою. Соңында, параметрлік бақылау алгоритмдері әдетте параметрлік емес мониторларды құру үшін ұқсас алгоритмдерді жалпылайды. Сондықтан, құрылған параметрлік емес мониторлардың сапасы алынған параметрлік мониторлардың сапасына әсер етеді. Алайда, басқа тексеру тәсілдерінен (мысалы, модельді тексеру) өзгеше, күйлер саны немесе құрылған монитордың мөлшері реттеу уақытында тексеруде маңызды емес; шын мәнінде, кейбір мониторларда шексіз көп күйлер болуы мүмкін, мысалы, жоғарыдағы SafeLock қасиеті үшін, бірақ кез келген уақытта тек шекті сандағы күйлер ғана болуы мүмкін. Маңыздысы - монитордың орындалатын жүйеден оқиға алған кезде бір күйден келесі күйге қаншалықты тиімді өтуі.

Improved instrumentation. Extracting events from the executing system and sending them to monitors can generate a large runtime overhead if done naively. Good system instrumentation is critical for any runtime verification tool, unless the tool explicitly targets existing execution logs. There are many instrumentation approaches in current use, each with its advantages and disadvantages, ranging from custom or manual instrumentation, to specialized libraries, to compilation into aspect oriented languages, to augmenting the virtual machine, to building upon hardware support. Combination with static analysis. A common combination of static and dynamic analyses, particularly encountered in compilers, is to monitor all the requirements that cannot be discharged statically. A dual and ultimately equivalent approach tends to become the norm in runtime verification, namely to use static analysis to reduce the amount of otherwise exhaustive monitoring. Static analysis can be performed both on the property to monitor and on the system to be monitored. Static analysis of the property to monitor can reveal that certain events are unnecessary to monitor, that the creation of certain monitors can be delayed, and that certain existing monitors will never trigger and thus can be garbage collected. Static analysis of the system to monitor can detect code that can never influence the monitors. For example, when monitoring the HasNext property above, one needs not instrument portions of code where each call i. next is immediately preceded on any path by a call i. hasnext that returns true (visible on the control flow graph). Efficient monitor generation and management. When monitoring parametric properties like the ones in the examples above, the monitoring system needs to keep track of the status of the monitored property with respect to each parameter instance. The number of such instances is theoretically unbounded and tends to be enormous in practice. An important research challenge is how to efficiently dispatch observed events to precisely those instances that need them. A related challenge is how to keep the number of such instances small (so that dispatching is faster), or in other words, how to avoid creating unnecessary instances for as long as possible and, dually, how to remove already created instances as soon as they become unnecessary. Finally, parametric monitoring algorithms typically generalize similar algorithms for generating non parametric monitors. Thus, the quality of the generated non parametric monitors dictates the quality of the resulting parametric monitors. However, unlike in other verification approaches (e. g., model checking), the number of states or the size of the generated monitor is less important in runtime verification; in fact, some monitors can have infinitely many states, such as the one for the SafeLock property above, although at any point in time only a finite number of states may have occurred. What is important is how efficiently the monitor transits from a state to its next state when it receives an event from the executing system.

Қасиеттерді анықтау

Барлық ресми тәсілдердің негізгі практикалық кедергілерінің бірі – олардың қолданушылары спецификацияларды оқуға немесе жазуға құлшынбайды, немесе қалай оқу және жазу керектігін білмейді және үйренуге ниеттемейді. Кейбір жағдайларда спецификациялар жасырын болады, мысалы, тұйыққа түсу және деректердің қақтығысуы сияқты жағдайларда, бірақ көбінесе оларды жасау қажет. Әсіресе, орындалу уақытында тексеру контекстінде, қосымша ыңғайсыздық – көптеген қолданыстағы спецификация тілдері мақсатталған қасиеттерді түсіруге жеткілікті деңгейде экспрессивті емес. Жақсы формализмдер. Орындалу уақытында тексеру қауымдастығында орындалу уақытында тексеруге қажетті қолданба салаларына жақсырақ сәйкес келетін спецификация формализмдерін жобалауға көп еңбек жұмсалды. Олардың кейбіреулері дәстүрлі формализмдерге шамалы немесе ешқандай синтаксистік өзгерістерді енгізбейді, бірақ олардың семантикасына ғана өзгерістер енгізеді (мысалы, шекті ізге қарсы шексіз із семантикасы және т.б.) және оларды жүзеге асыруға (Büchi автоматтарының орнына оңтайландырылған күйлі автоматтары және т.б.). Басқалары қолданыстағы формализмдерді орындалу уақытында тексеруге ыңғайлы, бірақ жоғарыда көрсетілген мысалдарда көрсетілгендей, параметрлерді қосу сияқты басқа тексеру тәсілдері үшін оңай болмауы мүмкін мүмкіндіктермен кеңейтеді. Соңында, орындалу уақытында тексеру үшін арнайы жобаланған спецификация формализмдері бар, олар осы сала үшін ең жақсы нәтижеге қол жеткізуге тырысады және басқа қолданба салаларына көп көңіл бөлмейді. Орындалу уақытында тексеру үшін жалпыға бірдей жақсы немесе салалық тұрғыдан жақсы спецификация формализмдерін жобалау және одан әрі дамыту оның маңызды зерттеу міндеттерінің бірі болып табылады. Сандық қасиеттер. Басқа тексеру тәсілдерімен салыстырғанда, орындалу уақытында тексеру жүйе күйінің айнымалыларының нақты мәндерімен жұмыс істей алады, бұл бағдарламаның орындалуы туралы статистикалық ақпаратты жинауға және осы ақпаратты күрделі сандық қасиеттерді бағалау үшін пайдалануға мүмкіндік береді. Бұл мүмкіндікті толыққанды пайдалануға мүмкіндік беретін көбірек экспрессивті қасиет тілдері қажет. Жақсы интерфейстер. Құрылымдық ерекшеліктерді оқу және жазу маман емес адамдар үшін оңай емес. Тіпті сарапшылар да салыстырмалы түрде кішкентай уақытша логикалық формулаларды бірнеше минут бойы қарап отырады (әсіресе олар "дейін" операторларын қамтығанда). Маңызды зерттеу саласы – пайдаланушыларға қасиеттерді оңай түсінуге, жазуға және тіпті визуализациялауға мүмкіндік беретін әртүрлі спецификация формализмдері үшін қуатты пайдаланушы интерфейстерін әзірлеу болып табылады. Спецификацияларды табу. Пайдаланушыларға спецификацияларды жасауға көмектесетін қандай құралдық қолдау болмасын, олар, әсіресе олар тривиальды болғанда, спецификациялар жазуға мәжбүр болмаудан гөрі көңіл көшіруге бейім. Бақытымызға орай, әрекеттерді/оқиғаларды дұрыс пайдаланатын көптеген бағдарламалар бар. Егер осылай болса, онда осы дұрыс бағдарламаларды пайдалануды және олардан қажетті қасиеттерді автоматты түрде үйренуді қалау логикалық. Автоматты түрде табылған спецификациялардың жалпы сапасы қолмен жасалған спецификациялардан төмен болуы мүмкін болса да, олар соңғыларының бастапқы нүктесі ретінде немесе қателерді табуға бағытталған автоматты орындалу уақытында тексеру құралдарының негізі ретінде қызмет ете алады (жаман спецификация жалған оң немесе теріс нәтижелерге әкелген кезде, сынақ кезінде көбінесе қабылданады).

One of the major practical impediments of all formal approaches is that their users are reluctant to, or don't know and don't want to learn how to read or write specifications. In some cases the specifications are implicit, such as those for deadlocks and data races, but in most cases they need to be produced. An additional inconvenience, particularly in the context of runtime verification, is that many existing specification languages are not expressive enough to capture the intended properties. Better formalisms. A significant amount of work in the runtime verification community has been put into designing specification formalisms that fit the desired application domains for runtime verification better than the conventional specification formalisms. Some of these consist of slight or no syntactic changes to the conventional formalisms, but only of changes to their semantics (e. g., finite trace versus infinite trace semantics, etc.) and to their implementation (optimized finite state machines instead of Büchi automata, etc.). Others extend existing formalisms with features that are amenable for runtime verification but may not easily be for other verification approaches, such as adding parameters, as seen in the examples above. Finally, there are specification formalisms that have been designed specifically for runtime verification, attempting to achieve their best for this domain and caring little about other application domains. Designing universally better or domain specifically better specification formalisms for runtime verification is and will continue to be one of its major research challenges. Quantitative properties. Compared to other verification approaches, runtime verification is able to operate on concrete values of system state variables, which makes it possible to collect statistical information about the program execution and use this information to assess complex quantitative properties. More expressive property languages that will allow us to fully utilize this capability are needed. Better interfaces. Reading and writing property specifications is not easy for non experts. Even experts often stare for minutes at relatively small temporal logic formulae (particularly when they have nested "until" operators). An important research area is to develop powerful user interfaces for various specification formalisms that would allow users to more easily understand, write and maybe even visualize properties. Mining specifications. No matter what tool support is available to help users produce specifications, they will almost always be more pleased to have to write no specifications at all, particularly when they are trivial. Fortunately, there are plenty of programs out there making supposedly correct use of the actions/events that one wants to have properties about. If that is the case, then it is conceivable that one would like to make use of those correct programs by automatically learning from them the desired properties. Even if the overall quality of the automatically mined specifications is expected to be lower than that of manually produced specifications, they can serve as a start point for the latter or as the basis for automatic runtime verification tools aimed specifically at finding bugs (where a poor specification turns into false positives or negatives, often acceptable during testing).

Орындау үлгілері мен болжамды талдау

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

Әдептілікті өзгерту

Сынақтан немесе толыққанды тексеруден өзгеше, орындалу кезіндегі тексеру жүйеге анықталған бұзушылықтардан қайта конфигурациялау, микроқайта орнату немесе кейде «реттеу» немесе «басқару» деп аталатын, одан да нәзік араласу механизмдері арқылы қалпына келу мүмкіндігін ұсынады. Бұл техникаларды орындалу кезіндегі тексерудің қатаң аясында іске асыру қосымша қиындықтар тудырады. Іс-әрекеттерді сипаттау. Орындалатын өзгеріс пайдаланушыға қатысы жоқ іске асыру егжей-тегжейін білуді қажет етпейтіндей абстрактілі түрде көрсетілуі керек. Сонымен қатар, жүйенің тұтастығын сақтау үшін мұндай өзгеріс қашан жасалатынын анықтау қажет. Араласудың салдары туралы ойлау. Араласу жағдайды жақсартатынын немесе кем дегенде нашарлатпайтынын білу маңызды. Іс-әрекет интерфейстері. Бақылау құралдары сияқты, жүйеге іс-әрекет шақыруларын қабылдауға мүмкіндік беруіміз керек. Шақыру механизмдері міндетті түрде жүйенің іске асылу егжей-тегжейіне байланысты болады. Дегенмен, сипаттама деңгейінде пайдаланушыға қандай жағдайда қандай іс-әрекеттер қолданылуы керектігін анықтап, жүйеге кері байланыс берудің декларативтік жолын ұсынуымыз керек.

Аспектке бағдарланған бағдарламалау

Жүргізу уақытын тексеру саласындағы зерттеушілер бағдарламаны модульдік түрде аспаптау үшін аспектке бағдарланған бағдарламалауды пайдалану мүмкіндігін байқады. Аспектке бағдарланған бағдарламалау (AOP) көлденең қиылыс мәселелерді модульдендіруді жалпы түрде қолдайды. Жүргізу уақытын тексеру осындай мәселелердің бірі болып табылады және осылайша AOP-тің белгілі бір ерекшеліктерінен пайда көре алады. Аспектке бағдарланған мониторлардың сипаттамалары көбінесе декларативті болып келеді, сондықтан императивті бағдарламалау тілінде жазылған бағдарламалық өзгерту арқылы жасалған аспаптауға қарағанда оларды түсіну оңай. Бұдан әрі, статикалық талдаулар бағдарламаның басқа аспаптау түрлеріне қарағанда мониторинг аспектілерін оңайрақ талдай алады, себебі барлық аспаптау бір аспектіде жинақталған. Сондықтан көптеген қазіргі жүргізу уақытын тексеру құралдары ерекшеліктерді компиляторлар түрінде жасалған, олар жоғары деңгейдегі ерекшеліктерді қабылдап, аспектке бағдарланған бағдарламалау тілінде (мысалы, AspectJ) кодты шығарады.

Ресми тексерумен біріктіру

Іске асырылу уақытында тексеру, егер дәлелденген дұрыс қалпына келтіру кодымен бірге қолданылса, бағдарламаны тексеру үшін құнды инфрақұрылымды қамтамасыз ете алады, бұл соңғысының күрделілігін едәуір төмендетуі мүмкін. Мысалы, үйме сұрыптау алгоритмін формалды түрде тексеру өте қиын. Оны тексерудің оңайырақ тәсілі – оның нәтижесін сұрыпталған күйде бақылау (сызықтық күрделіліктегі монитор), егер сұрыпталмаса, оны оңай тексерілетін процедураны қолдана отырып сұрыптау, мысалы, енгізу сұрыптау. Нәтижесіндегі сұрыптау бағдарламасын тексеру оңайырақ, үйме сұрыптаудан талап етілетін жалғыз нәрсе – бастапқы элементтерді көп жиынтық ретінде қарастырғанда жоймауы, мұны дәлелдеу әлдеқайда оңай. Керісінше қарасақ, ресми тексеруді орындалу уақытында тексерудің шығындарын азайту үшін пайдалануға болады, бұл жоғарыда айтылғандай, ресми тексерудің орнына статикалық талдау үшін де қолданылады. Шындығында, толыққанды орындалу уақытында тексерілген, бірақ ыңғайсыз баяу бағдарламадан бастауға болады. Содан кейін формалды тексеруді (немесе статикалық талдауды) мониторларды алып тастау үшін қолдануға болады, дәл сол сияқты компилятор типінің дұрыстығын немесе жад қауіпсіздігін тексеруді орындалу уақытында жүргізбеу үшін статикалық талдауды пайдаланады.

Қақпақты арттыру

Дәстүрлі тексеру әдістерімен салыстырғанда, орындалу уақытында тексерудің бірден-бір кемшілігі – оның қамту аймағының төмендеуі. Бұл жүйемен бірге орнатылғанда (мүлік бұзылған кезде орындалатын тиісті қалпына келтіру кодымен бірге) мәселе тудырмайды, бірақ жүйедегі қателерді табу үшін қолданылғанда орындалу уақытында тексерудің тиімділігін шектеуі мүмкін. Қателерді анықтау мақсатында орындалу уақытында тексерудің қамту аймағын арттыру тәсілдері:

Кіріс деректерін жасау. Жақсы кіріс деректері жиынтығын (бағдарламаның кіріс айнымалыларының мәндері, жүйелік шақырулардың мәндері, жіптердің кестесі және т.б.) жасау тестілеудің тиімділігін едәуір арттыратыны белгілі. Бұл қателерді анықтау үшін қолданылатын орындалу уақытында тексеру үшін де жарамды, бірақ кіріс деректерін жасау процесін басқару үшін бағдарламалық кодты пайдаланумен қатар, орындалу уақытында тексеруде, егер қолжетімді болса, мүліктердің сипаттамаларын қолдануға және қажетті мінез-құлықты тудыру үшін бақылау техникаларын қолдануға болады. Орындалу уақытында тексеруді қолдану оны модельге негізделген тестілеумен тығыз байланысты етеді, бірақ орындалу уақытында тексеру сипаттамалары әдетте жалпы мақсаттағы болады, міндетті түрде тестілеу үшін жасалмайды. Мысалы, жоғарыдағы жалпы мақсаттағы UnsafeEnum мүлігін тексеруді қарастырайық. Жоғарыда аталған мониторды жүйелік орындалуды пассивті түрде бақылау үшін ғана жасаудың орнына, екінші e.nextElement оқиғасын жасауға тырысатын жіпті тоқтатып, басқа жіптердің бірі v.update оқиғасын жасауы мүмкін деген үмітпен орындалуына мүмкіндік беретін «ақылды» монитор жасауға болады, бұл жағдайда қате табылады. Динамикалық символдық орындау. Символдық орындауда бағдарламалар символдық түрде орындалады және бақыланады, яғни нақты кіріс деректері болмайды. Жүйенің бір символдық орындалуы нақты кіріс деректерінің үлкен жиынтығын қамтуы мүмкін. Қолжетімді шектеулерді шешу немесе қанағаттандыруды тексеру әдістері жиі символдық орындауды жүргізу немесе олардың кеңістігін жүйелі түрде зерттеу үшін қолданылады. Егер қанағаттандыруды тексеруші таңдау нүктесін өңдей алмаса, онда сол нүктеден өту үшін нақты кіріс дерегі жасалуы мүмкін; нақты және символдық орындаудың бұл комбинациясы конколик орындау деп те аталады.