Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем

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

Full description

Saved in:

Bibliographic Details
Date:	2008
Main Author:	Колчин, А.В.
Format:	Article
Language:	Russian
Published:	Інститут програмних систем НАН України 2008
Subjects:	Теоретичні та методологічні основи програмування
Online Access:	https://nasplib.isofts.kiev.ua/handle/123456789/2598
Tags:	Add Tag No Tags, Be the first to tag this record!
Journal Title:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Cite this:	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем / А.В. Колчин // Проблеми програмування. — 2008. — № 4. — С. 3-12. — Бібліогр.: 23 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

_version_	1860111304288632832
author	Колчин, А.В.
author_facet	Колчин, А.В.
citation_txt	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем / А.В. Колчин // Проблеми програмування. — 2008. — № 4. — С. 3-12. — Бібліогр.: 23 назв. — рос.
collection	DSpace DC
description	Предложен метод направленного поиска для автоматического построения тестовых сценариев в процессе верификации. Метод использует определяемые пользователем в виде регулярных выражений цели тестирования и ограничения обхода поведения модели. Описаны стратегии управления поиском и техника ослабления эквивалентности трасс и состояний. Запропоновано метод спрямованого пошуку для автоматичної побудови тестових сценаріїв у процесі верифікації. Метод використовує цілі тестування та обмеження на обхід поведінки моделі, які визначає користувач у вигляді регулярних виразів. A guided search method for automatic test scenario building during verification proposed. The method uses user-defined regular expressions as test purposes and for model behavior traversal bounding. Search managing strategies together with trace and state equivalence weakening described.
first_indexed	2025-12-07T17:34:12Z
format	Article
fulltext	Теоретичні та методологічні основи програмування © А.В. Колчин, 2008 ISSN 1727-4907. Проблеми програмування. 2008. № 4 5 УДК 519.686.2 А.В. Колчин МЕТОД НАПРАВЛЕНИЯ ПОИСКА И ГЕНЕРАЦИИ ТЕСТОВЫХ СЦЕНАРИЕВ ПРИ ВЕРИФИКАЦИИ ФОРМАЛЬНЫХ МОДЕЛЕЙ АСИНХРОННЫХ СИСТЕМ Предложен метод направленного поиска для автоматического построения тестовых сценариев в процессе верификации. Метод использует определяемые пользователем в виде регулярных выражений цели тестирования и ограничения обхода поведения модели. Описаны стратегии управления поиском и техника ослабления эквивалентности трасс и состояний. Введение Техника формальной верификации, получившая название проверки модели (model checking [1]), является одним из наиболее перспективных и широко ис- пользуемых подходов к решению про- блемы автоматизации проверки правиль- ности программ. В настоящее время наиболее популярны такие системы: SPIN [2], SMV [3], NuSMV [4], VeriSoft [5]. К недостаткам верификации можно отнести проблему комбинаторного взрыва числа состояний, а так же тот факт, что свойства проверяются на модели, а не на реальной системе. Для проверки соответствия требо- ваниям реальной системы выполняется тестирование. Так как при тестировании проверить поведение программы во всех ситуациях невозможно, прибегают к опре- делению критериев покрытия и ограничи- ваются требованием проверки классов тес- товых сценариев, удовлетворяющих таким критериям. Трудоемкость создания тестов по функциональным спецификациям вруч- ную (или с применением симуляторов) не приемлема для систем со сложной моделью поведения. Обостряется необ- ходимость не только верификации моделей систем, но и автоматизации создания тес- товых сценариев. Системы, позволяющие автоматизиро- вать построение тестовых наборов на этапе верификации обычно оценивают полноту покрытия тестовым набором по следую- щим метрикам и критериям: число выпол- ненных операторов программы, ветвей, путей, число проверенных состояний дан- ных и переходов между состояниями, пок- рытие граничных значений функций и пре- дикатов модели, и др. Генерация тестовых сценариев поддерживается многими инст- рументами, использующими автоматные модели целевой системы. Такие инстру- менты хорошо подходят для верификации систем, при разработке которых исполь- зуются формальные языки спецификаций, например, SDL [6], LOTOS [7], Estelle [8]. Вопрос о том, в каком соотношении нахо- дятся показатели тестового покрытия мо- дели и требований к целевой системе в общем случае, как правило, не рассматри- вается. Таким образом, соответствия меж- ду полученными тестовыми сценариями, которые удовлетворяют вышеописанным критериям, и основными требованиями на функциональность целевой системы нет. Системы верификации [2–4] предпола- гают, что свойство, которое необходимо проверить на модели, задано в виде некото- рой формулы темпоральной логики. Этим можно было бы воспользоваться, сфор- мулировав такую формулу, которая станет ложной на некотором пути (такой путь бу- дет выдан верификационной системой в качестве контр-примера), и при этом путь будет рассматриваться как тестовый сцена- рий, покрывающий некоторое требование. Однако, на практике однозначного соот- ветствия между состоянием (значением атрибутов), описываемым такой формулой и желаемой последовательностью событий нет; более того, высокий уровень необхо- димых знаний в области математической логики, предъявляемый пользователю, час- то является существенным ограничиваю- щим фактором, усложняющим использова- ние формальных методов в процессе про- Теоретичні та методологічні основи програмування 6 мышленной разработки программного обеспечения. В работах [9, 10, 12] помимо спецификаций поведения системы, на вход подается сценарий тестирования, назы- ваемый обычно целью теста (test purpose), такой сценарий задается пользователем в виде последовательности сообщений, ко- торыми обмениваются компоненты моде- ли, например, в виде MSC [10, 11]. Направленный поиск и создание тестовых сценариев Описываемый в данной работе метод позволяет пользователю задавать критерии покрытия, которые будут одновременно служить направлением поиска трасс для тестовых сценариев при обходе пространс- тва поведения модели. В отличие от [2–4] желаемые свойства системы формули- руются в терминах событий модели; в от- личие от [12] метод не подразумевает вне- сения изменений в постусловия переходов исходной модели. Заметим так же, что ве- рификация в системах [9, 10, 12] выпол- няется с фиксированным ограничением на длину трассы, таким образом, отсутствие результата не означает, что модель не до- пускает тестовый сценарий. Описываемый метод подразумевает накладывание огра- ничений на тестовый сценарий, что дает возможность проверить его допустимость. Еще одним важным отличием является то, что такие сценарии накладывают дополни- тельные ограничения на поиск, отсекая ветви поведения модели, не удовлетворяю- щие тестовому сценарию. Метод можно использовать в качестве определяемой пользователем эвристики при решении задач достижимости [13, 14]. Далее предложено расширение спосо- бов описания цели теста путем задания специальных регулярных выражений над алфавитом имен параметризированных пе- реходов модели (далее образцов), опреде- ляющих условие покрытия и направление поиска. Операционная семантика специфика- ций может быть определена в терминах транзиционных систем. Транзиционная система – это тройка ),,( 0 →= qQT , где Q – множество состояний, Qq ∈0 – на- чальное состояние, QQ ×→⊆ – множество переходов, записывается qq ′→ . Путь из состояния 0q в nq – (конечная) последова- тельность состояний nqqq →→→ ...10 . Состояние q достижимо, если существует путь из 0q в q . Размеченная транзицион- ная система ),( ATTL = где ),,( 0 →= qQT – транзиционная система, в которой множество переходов имеет разметку: U →→= ∈ a Aa . Трасса в TL это последо- вательность ,...,..., 21 naaa такая, что сущес- твует путь ......21 10 n aaa qqq n→→→ Язык, ассоциированный с TL обозначается L )(TL – это набор всех трасс, выходящих из начального состояния. Как правило, со- бытия формальной модели ассоциируются с именами ее переходов, поэтому в данной работе множеством меток A является мно- жество параметризированных имен пере- ходов. Каждый переход на трассе парамет- ризирован идентификатором инстанции (процесса). Цели тестирования задаются пользователем в виде образцов следую- щего вида: na. – переход a с любым параметром на максимальной дистанции n ; nia ).( – переход a с параметром i на максимальной дистанции n ; a~ – запрет перехода a с любым па- раметром; )(~ ia – запрет перехода a с парамет- ром i ; ba; – операция конкатенации образ- цов; ba ∨ – недетерминированный выбор образцов; ba \|\| – параллельная композиция об- разцов; a – итерация образца a . Назовем переходы, входящие в образец, наблюдаемыми. Два наблю- даемых перехода на трассе расположены на дистанции x , если между ними распо- ложены 1−x переходов. Дистанция перво- го перехода в образце является расстоя- нием от начального состояния. Запреты действуют до обнаружения следующего допустимого наблюдаемого перехода и не Теоретичні та методологічні основи програмування 7 могут быть последними в образце (за исключением использования внутри итера- ции). Параллельная композиция образцов используется для случаев, когда модель имеет несколько параллельно работающих компонент (процессов), причем дистанция подсчитывается для каждого параллельно- го участка образца отдельно. Построенная трасса удовлетворяет образцу, если она содержит переходы в непротиворечащей заданному образцу последовательности, на дистанциях, не превышающих указанные. Например, образец )4.);1(~2.(;2).1( trCmstrZtrBmstrA ∨ имеет примеры удовлетворяющих трасс: )2(),1(),1(),1( mstrBmstrZmstrAmstrS , )2(),1(),1( mstrCmstrXmstrA пример не удовлетворяющей трассы: )1(),2(),1(),1(),1( mstrBmstrCmstrZmstrXmstrA Как видно, выражения, не содержащие итерации, всегда имеют максимальную длину трассы, удовлетворяющей образцу; более того, в отличие от [9], определить, что трасса не удовлетворяет образцу, мож- но не достигая этого максимума, так как всегда определена максимальная дистан- ция между событиями. В приведенном примере максимальная длина трассы 6, в то время как трасса )1(),1(),1( mstrCmstrZmstrA уже не имеет допустимого образцом про- должения и может быть прервана. Семантически такие образцы задают «контрольные точки» поведения модели и так же определяют критерий выбора пост- роенных трасс (вариантов конкретного по- ведения системы) для последующего их использования в качестве тестовых сцена- риев [14]. Так, предполагаемые поведения моделируемой системы, описанные поль- зователем, проверяются на допустимость, одновременно накладывая ограничения на поиск. По заданным образцам строится соответствующий детерминированный ко- нечный автомат. Для различных видов ре- гулярных выражений существуют алгорит- мы различной вычислительной сложности [15, 16]. Заметим, что на практике удовлет- ворительный результат можно получить, используя жадные алгоритмы линейной сложности. Обход пространства поведения, реализующий адаптированный алгоритм Тарьяна [17], модифицируется путем доба- вления перед шагом вглубь вызова специальной функции, реализующей авто- мат, распознающий образцы, при этом полным состоянием модели будет синхрон- ное произведение состояний модели (знач- ений атрибутов) и состояний автомата, распознающего образцы. Если текущая трасса удовлетворяет образцу, она будет сохранена на жесткий диск, если не исчер- пан соответствующий лимит (пользователь определяет нужное количество трасс по каждому образцу). Если лимит исчерпан, образец исключается из списка актуаль- ных. Если данная функция возвращает на выходе false, это означает, что достиг- нута ситуация, из которой любое продол- жение текущей трассы не приведет обна- ружению вхождения очередного символа (имени наблюдаемого перехода) хотя бы одного актуального образца. Такая ситуа- ция является дополнительным критерием завершения генерации текущей трассы, таким образом, алгоритм выполнит шаг назад. При этом, если трасса содержит исторически максимальной длины префикс хотя бы одного образца, она будет сохра- нена на диск с соответствующей пометкой. Таким образом, если полного вхождения какого-либо образца не обнаружено, будет построена трасса, удовлетворяющая мак- симальному префиксу этого образца. Дополнительным для сохранения трассы является условие вхождения в трассу перехода, не входящего ни в одну из уже сохраненных трасс. В итоге будет пост- роен набор трасс, включающий как пред- полагаемые пользователем поведения мо- дели, так и все достигнутые переходы модели. Теоретичні та методологічні основи програмування 8 Использование итерации Для обнаружения бесконечных циклов используется итерация (замыкание Клини). Допускается использование не более одной итерации и только в конце образца. Необходимо отметить, что под циклом в данном случае понимается цикл полных состояний, т.е. состояний автомата регу- лярного выражения и значений атрибутов модели. Например, используя итерацию, можно проверить, приходит ли модель системы в устойчивое состояние при отсутствии внешних сигналов. Пусть trE1 и trE2 – единственные воздействия (переходы) вне- шней среды, а trA – переход некоторого единственного процесса ms. Пусть так же задан образец 1(~;4).(;2.1 trEmstrAtrE \|\| )2~ trE Тогда трасса, удовлетворяющая образ- цу должна иметь цикл, в котором нет пере- ходов trE1 и trE2, а префикс этой трассы должен включать переходы trE1 и trA(ms) на соответствующих дистанциях. Таким образом, после воздействия среды собы- тием, размеченным переходом trE1 и пос- ледующей реакцией переходом trA, про- цесс ms не приходит в устойчивое состоя- ние (в цикл не входит ни одно событие от внешней среды). Стратегии Одним из подходов к решению про- блемы комбинаторного взрыва является привлечение пользователя (эксперта пред- метной области) к процессу верификации. Большинство из верификационных систем использует заданные пользователем абст- ракции [18] и специальные состояния, описанные в виде формул темпоральной логики для отсечения ветвей поведения («hints», «restricted states», «fairness const- raints») [19, 20]. В работе [21] предложен метод автоматического направления поис- ка нарушения свойств модели, в основе которого лежит структурный анализ пере- ходов модели и проверяемых свойств. В работе [22] описан верификатор, исполь- зующий эвристические методы для нап- равления поиска ошибок модели. В отли- чие от упомянутых, данная работа предла- гает интерфейс к правилам и инструкциям обхода пространства поведения модели, посредством которого пользователь может задавать свои эвристики в терминах пере- ходов (событий) модели. По заданным пра- вилам строится автомат, работающий син- хронно с автоматом распознавания образ- цов, динамически изменяющий ограниче- ния пространства поиска (длина трассы, терминальные состояния), приоритеты для инстанций (процессов) и переходов, а так же реализующий механизмы включения и выключения инстанций и переходов на не- которых участках поведения модели. Тело основного цикла поиска в глубину моди- фицируется путем добавления предвари- тельной сортировки переходов в соответс- твии с приоритетами и исключения вы- ключенных переходов. Ослабление эквивалентности трасс В данном случае ослабление трассовой эквивалентности подразумевает разделе-ние модели на тестируемую и тестирую-щую инстанции. Такой подход применим в случае, когда переходы модели представ-ляют собой тройки вида BA p→ , где A и B пред- и предусловия, а p описывает процесс – наблюдаемые события перехода. В работах [14, 23] процесс описывается MSC диаграммой, а результирующая трас-са записывается в виде MSC сценария, сос- тоящего из последовательности событий соответствующих трассе переходов. Так, для ослабления эквивалентности, пользо- ватель выделяет два набора инстанций, после чего трассовая эквивалентность рассматривается с точностью до событий тестируемых инстанций. Описанная далее процедура Save_Abstract_Trace стро- ит абстрактные трассы, используя задан- ную эквивалентность. Трасса состоит из переходов модели, которые в свою очередь описывают события, причем не обяза- тельно одной инстанции (процесса). Функ- ция instance идентифицирует инстанцию очередного события на трассе. Теоретичні та методологічні основи програмування 9 Вход: полная трасса Trace, множество тестируемых инстанций Tested_Instances и идентификатор теста Test_ID. Выход: абстрактная трасса Abstract_ Trace. Save_Abstract_Trace := proc(Trace, Tested_Instances, Test_ID) local(Abstract_Trace, Transition, Event) begin Abstract_Trace ← ∅; for_each Transition ∈ Trace do for_each Event ∈ Transition do if(instance(Event) ∈ Tested_Instances) do Abstract_Trace ← {Abstract_Trace ∪ Event}; Save_Trace(Abstract_Trace, Test_ID) end На практике актуальна минимизация чис- ла тестов. Процедура Save_Trace обес- печивает поиск вхождения одного теста в другой. В случае обнаружения, новая трас- са либо не добавляется к тестовым сцена- риям, либо заменяет ранее добавленный. Вход: абстрактная трасса Abstract_Trace и идентификатор теста Test_ID. Выход: обновленное множество Stored. Save_Trace := proc(Abstract_Trace, Test_ID)local(T) begin for_each T ∈ Stored do begin if(Abstract_Trace ⊆ T.trace) do return; if (Abstract_Trace ⊃ T.trace) do begin T.trace ← Abstract_Trace; T.test_id ← {T.test_id ∪ Test_ID}; return end end Stored ← {Stored ∪ (Abstract_Trace, Test_ID)} end В результате множество Stored будет содержать минимизированный набор пар состоящих из абстрактной трассы и списка идентификаторов тестовых целей. Ослабление эквивалентности состояний Ослабление эквивалентности состоя- ний в данном случае является дополни- тельной возможностью для пользователя задавать стратегию поиска путем опреде- ления правил абстракции состояний. Такие правила представляют собой условия для игнорирования либо изменения значений некоторых атрибутов пройденных состоя-ний. Например, для системы, в которой после заполнения информации в полях некоторого интерфейсного диалогового окна была выполнена команда «отменить», введенные значения не играют роли, и в следующий раз при выполнении такой ко-манды состояние модели будет идеентифи-цировано как пройденное, если найдется пройденное ранее состояние, эквивалент-ное данному без учета значений полей диа-лога. Далее приведен пример такой функ-ции user_abstraction, определяемой пользователем. Вход: конкретное состояние модели Выход: абстрактное состояние, построенное согласно правилам пользователя user_abstraction := proc(S)local(A)begin Теоретичні та методологічні основи програмування 10 A ← S; if(S.command = “cancel”) do ignore(A, Dialog.data); if(S.command = “send_sms” & S.sms_size > S.max_sms_size) do A.sms_size ← S.max_sms_size + 1 return A end Заметим, что в данном примере второе правило абстрагирует реальное значение атрибута, хранившего размер сообщения. Таким образом пользователь сообщает системе, что нет смысла различать размер сообщения, превосходящего максимально допустимый, и что в таком случае дос- таточно лишь зафиксировать факт превы- шения допустимого значения. Функция ignore исключает атрибут (Dialog. .data) из состояния (A). Описанная далее процедура исполь-зуется для сохранения и проверки прой-денных состояний с учетом пользователь-ских абстракций; применяется в процессе обхода поведения модели. Вход: конкретное состояние модели Выход: обновленное абстрактным состоя-нием множество Visited visited := proc(S)local(v)begin for_each v ∈ Visited do begin flag ← true; for_each a ∈ v do if(v->a.value ≠ S->a.value) do begin flag ← false; break end if(flag = true) do return true end v ← user_abstraction(S); Visited ← {Visited ∪ v}; return false end Пример Далее приведена типичная тестовая процедура и соответствующий тестовый сценарий из промышленного телекомму- никационного проекта [14]. Вход: тестовая процедура (последователь- ность действий): 1) X создает Y; 2) X про- веряет, что Y создан; 3) X удаляет Y; 4) X и Y получают уведомление об удалении; 5) X проверяет, что Y больше нет в списке контактов; 6) Y проверяет, что X больше нет в списке контактов. В результате по тестовой процедуре было построено такое выражение, задающее цель тестирования: sec_T1943 = ( create_contact(ms1).30 ; PTT_Contacts04(ms1).10 \/ PTT_Contacts05(ms1).10 ; PTT_Accept_Invitation(ms2).15 ; show_indiv_cont(ms1).10 ; delete_indiv_cont(ms1).3 ; PTT_Receive_Notice06(ms1).7 \|\| PTT_Receive_Notice07(ms2).7 ; show_empty_indiv_cont(ms1).10 \|\| show_ empty_indiv_cont(ms2).10 ) Теоретичні та методологічні основи програмування 11 Выход: трасса (тестовый сценарий): пол- ная последовательность событий модели, соответствующая тестовой процедуре. Применение технологии направленного поиска дало возможность не только выя- вить ошибки в спецификациях, но и соз- дать набор тестовых сценариев (~100 трасс), обеспечивающих необходимое функциональное покрытие. События MSC трассы были транслированы в последо- вательности команд тестируемого устрой- ства, что дало возможность автоматизиро- вать исполнение построенных таким методом тестов [14]. Выводы Предложенный метод является разно- видностью ограниченной проверки модели (bounded model checking), в качестве огра- ничителей использует цели тестирования, определяемые пользователем. Метод про- веряет допустимость предполагаемых по- ведений, по сути осуществляя валидацию модели. Использование коротких дистан- ций и запретов между контрольными точ- ками образцов позволяет эффективно на- ходить труднодостижимые состояния. Ме- тоды ослабления эквивалентности трасс и состояний существенно сокращают коли- чество тестовых сценариев обеспечиваю- щих необходимое покрытие и время поиска. 1. http://en.wikipedia.org/wiki/Model_checking 2. Ben-Ari. M. Principles of Spin. // Springer Verlag. – 2008. – P. 216. 3. Burch J., Clarke E., McMillan K., Dill D., and Hwang L. Symbolic model checking: 10^20 states and beyond // Information and Computation. – 1992. – Vol. 98, N 2. – P. 142–170. 4. Cimatti A., Clarke E., Giunchiglia E., and others. NuSMV 2: An OpenSource Tool for Symbolic Model Checking // In Proceeding of International Conf. on Computer-Aided Verification, Copenhagen, Denmark. – 2002. – P. 359–364. 5. Godefroid P. Partial-order methods for the verification of concurrent systems – an approach to the state-explosion problem // Lecture notes in computer science, Springer-Verlag. – 1996. – Vol. 1032. – P. 143. 6. ITU-T Recommendation Z.100 – Specification and Description Language (SDL), ITU. – 2002. 7. ISO/IEC. Information Processing Systems - Open Systems Interconnection – LOTOS – A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807:1989, International Organization for Standardization, Geneva, Switzerland. – 1989. 8. ISO/TC97/SC21. Information Processing Systems – Open Systems Interconnection – Estelle – A Formal Description Technique based on an Extended State Transition Model. ISO 9074:1997, International Organization for Standardization, Geneva, Switzerland. –1997. 9. Fernandez J., Jard C., Jeron T., Nedelka L., and Viho C. An experiment in automatic generation of test suites for protocols with verification technology // Science of Computer Programming. – 1997. – Vol. 29, N 1–2. – P. 123–146. 10. Grabowski J., Hogrefe D., Nahm R. Test case generation with test purpose specification by MSCs // In Elsevier Science B.V. (North-Holland), editor, 6th SDL Forum. – 1993. – P. 253–266. 11. ITU-T Recommendation Z.120 – Message Sequence Chart (MSC), ITU. – 1996. 12. Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A. UniTesK Test Suite Architecture // In Proc. of FME 2002, LNCS 2391, Springer-Verlag. – 2002. – P. 77–88. 13. Колчин А.В. Направленный поиск в верификации формальных моделей // Тези доп. Міжнар. конф. «Теоретичні та прикладні аспекти побудови програмних систем TAAPSD'2007». – К.: НаУКМА, Національний ун-т ім. Т.Г. Шевченка, Інститут програмних систем НАН України. – 2007. – С. 256–258. 14. Баранов С.Н., Котляров В.П., Летичевский А.А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований // Труды Междунар. науч. конф. «Космос, астрономия и программирование». – С-Пб: СПбГУ, 2008. – С. 134–145. 15. Aho A. Algorithms for finding patterns in strings // Handbook for theoretical computer science, MIT Press. – 1990. – Vol. A. – P. 257–300. 16. Smyth B. Computing Patterns in Strings // ACM Press Books. – 2003. – P. 440. 17. Колчин А.В. Автоматический метод оператив- ного построения абстракций при верификации формальных моделей асинхронных систем // Искусственный интеллект. – 2008. – № 4. – С. 690–705. 18. Clarke E. Model checking and abstraction // In ACM Transactions on programming languages and systems. – 1994. – Vol. 16, N 5. – P. 1512–1542. 19. Bloem R., Ravi K., and Somezi F. Symbolic guided search for CTL model checking // In Design Automation Conference. – 2004. – P. 29–34. 20. Barner S., Glazberg Z., and Rabinovitz I. Wolf - bug hunter for concurrent software using formal Теоретичні та методологічні основи програмування 12 methods // In Computer Aided Verification. – 2005. – P. 153–157. 21. Peranandam P., Weiss R., Ruf J., Kropf T. and Rosenstiel W. Dynamic guiding of bounded property checking // In IEEE International High Level Design Validation and Test Workshop. – 2004. – P. 15–18. 22. Edelkamp, S., Leue S., and Lafuente A. L. Directed explicit-state model checking in the validation of communication protocols // International journal on software tools for technology transfer. – 2003. – N 5. – P. 247–267. 23. Baranov S.N., Kapitonova J.K., Kolchin A.V., and others. Tools for Requirements Capturing Based on the Technology of Basic Protocols // Proc. of St. Petersburg IEEE Chapter. – 2005. – P. 92–97. Получено 04.06.2008 Об авторе: Колчин Александр Валентинович, младший научный сотрудник. Место работы автора: Институт кибернетики им. В.М. Глушкова НАН Украины. Тел.: (044) 200 8423. e-mail: kolchin_av@yahoo.com
id	nasplib_isofts_kiev_ua-123456789-2598
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn	1727-4907
language	Russian
last_indexed	2025-12-07T17:34:12Z
publishDate	2008
publisher	Інститут програмних систем НАН України
record_format	dspace
spelling	Колчин, А.В. 2008-12-15T13:20:30Z 2008-12-15T13:20:30Z 2008 Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем / А.В. Колчин // Проблеми програмування. — 2008. — № 4. — С. 3-12. — Бібліогр.: 23 назв. — рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2598 519.686.2 Предложен метод направленного поиска для автоматического построения тестовых сценариев в процессе верификации. Метод использует определяемые пользователем в виде регулярных выражений цели тестирования и ограничения обхода поведения модели. Описаны стратегии управления поиском и техника ослабления эквивалентности трасс и состояний. Запропоновано метод спрямованого пошуку для автоматичної побудови тестових сценаріїв у процесі верифікації. Метод використовує цілі тестування та обмеження на обхід поведінки моделі, які визначає користувач у вигляді регулярних виразів. A guided search method for automatic test scenario building during verification proposed. The method uses user-defined regular expressions as test purposes and for model behavior traversal bounding. Search managing strategies together with trace and state equivalence weakening described. ru Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем A method for guided search and test scenarios generation in verification of formal models of asynchronous systems Article published earlier
spellingShingle	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем Колчин, А.В. Теоретичні та методологічні основи програмування
title	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем
title_alt	A method for guided search and test scenarios generation in verification of formal models of asynchronous systems
title_full	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем
title_fullStr	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем
title_full_unstemmed	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем
title_short	Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем
title_sort	метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем
topic	Теоретичні та методологічні основи програмування
topic_facet	Теоретичні та методологічні основи програмування
url	https://nasplib.isofts.kiev.ua/handle/123456789/2598
work_keys_str_mv	AT kolčinav metodnapravleniâpoiskaigeneraciitestovyhscenarievpriverifikaciiformalʹnyhmodeleiasinhronnyhsistem AT kolčinav amethodforguidedsearchandtestscenariosgenerationinverificationofformalmodelsofasynchronoussystems

Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем

Institution

Similar Items