Static method of consistency and completeness checking in formal model of distributed software systems

Static method of consistency and completeness checking in formal model of distributed software systems

The paper describes a new method for discovering of incompleteness, inconsistency and race conditions in formal models. The method implements the properties checking basing on model transitions description, and does not traverse model state space.Prombles in programming 2014; 2-3: 145-150

Збережено в:
Бібліографічні деталі
Дата:2025
Автори: Kolchin, A.V., Letichevsky, O.O., Potiyenko, S.V.
Формат: Стаття
Мова:Russian
Опубліковано: PROBLEMS IN PROGRAMMING 2025
Теми:
UDC 004.415.5
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/705
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-705
record_format ojs
resource_txt_mv ppisoftskievua/e0/0d6a8bb4f1b5f1ce95eb1955e24b05e0.pdf
spelling pp_isofts_kiev_ua-article-7052025-04-09T22:22:32Z Static method of consistency and completeness checking in formal model of distributed software systems Метод статической проверки полноты и непротиворечивости в формальных моделях распределенных программных систем Kolchin, A.V. Letichevsky, O.O. Potiyenko, S.V. UDC 004.415.5 УДК 004.415.5 The paper describes a new method for discovering of incompleteness, inconsistency and race conditions in formal models. The method implements the properties checking basing on model transitions description, and does not traverse model state space.Prombles in programming 2014; 2-3: 145-150 Описан метод выявления таких патологий формальных моделей, как неполнота и противоречивость, а так же гонки в параллельных процессах. Метод реализует проверку свойств на основании анализа описания переходов модели, при этом не строит пространство ее состояний.Prombles in programming 2014; 2-3: 145-150 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-04-09 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/705 PROBLEMS IN PROGRAMMING; No 2-3 (2014); 146-150 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2014); 146-150 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2014); 146-150 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/705/757 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2025-04-09T22:22:32Z
collection OJS
language Russian
topic
UDC 004.415.5
spellingShingle
UDC 004.415.5
Kolchin, A.V.
Letichevsky, O.O.
Potiyenko, S.V.
Static method of consistency and completeness checking in formal model of distributed software systems
topic_facet
UDC 004.415.5

УДК 004.415.5
format Article
author Kolchin, A.V.
Letichevsky, O.O.
Potiyenko, S.V.
author_facet Kolchin, A.V.
Letichevsky, O.O.
Potiyenko, S.V.
author_sort Kolchin, A.V.
title Static method of consistency and completeness checking in formal model of distributed software systems
title_short Static method of consistency and completeness checking in formal model of distributed software systems
title_full Static method of consistency and completeness checking in formal model of distributed software systems
title_fullStr Static method of consistency and completeness checking in formal model of distributed software systems
title_full_unstemmed Static method of consistency and completeness checking in formal model of distributed software systems
title_sort static method of consistency and completeness checking in formal model of distributed software systems
title_alt Метод статической проверки полноты и непротиворечивости в формальных моделях распределенных программных систем
description The paper describes a new method for discovering of incompleteness, inconsistency and race conditions in formal models. The method implements the properties checking basing on model transitions description, and does not traverse model state space.Prombles in programming 2014; 2-3: 145-150
publisher PROBLEMS IN PROGRAMMING
publishDate 2025
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/705
work_keys_str_mv AT kolchinav staticmethodofconsistencyandcompletenesscheckinginformalmodelofdistributedsoftwaresystems
AT letichevskyoo staticmethodofconsistencyandcompletenesscheckinginformalmodelofdistributedsoftwaresystems
AT potiyenkosv staticmethodofconsistencyandcompletenesscheckinginformalmodelofdistributedsoftwaresystems
AT kolchinav metodstatičeskojproverkipolnotyineprotivorečivostivformalʹnyhmodelâhraspredelennyhprogrammnyhsistem
AT letichevskyoo metodstatičeskojproverkipolnotyineprotivorečivostivformalʹnyhmodelâhraspredelennyhprogrammnyhsistem
AT potiyenkosv metodstatičeskojproverkipolnotyineprotivorečivostivformalʹnyhmodelâhraspredelennyhprogrammnyhsistem
first_indexed 2025-07-17T09:58:15Z
last_indexed 2025-07-17T09:58:15Z
_version_ 1850410419222478848
fulltext Формальні методи програмування © А.В. Колчин, А.А. Летичевский, С.В. Потиенко, 2014 146 ISSN 1727-4907. Проблеми програмування. 2014. № 2–3. Спеціальний випуск УДК 004.415.5 МЕТОД СТАТИЧЕСКОЙ ПРОВЕРКИ ПОЛНОТЫ И НЕПРОТИВОРЕЧИВОСТИ В ФОРМАЛЬНЫХ МОДЕЛЯХ РАСПРЕДЕЛЕННЫХ ПРОГРАММНЫХ СИСТЕМ А.В. Колчин, А.А. Летичевский, С.В. Потиенко Институт кибернетики им. В.М. Глушкова НАН Украины, 03680, Киев, проспект Академика Глушкова, 40. E-mail: kolchin_av@yahoo.com, Oleksandr.Letychevskyy@iss.org.ua, Stepan.Potiyenko@iss.org.ua Описан метод выявления таких патологий формальных моделей, как неполнота и противоречивость, а так же гонки в параллельных процессах. Метод реализует проверку свойств на основании анализа описания переходов модели, при этом не строит пространство ее состояний. The paper describes a new method for discovering of incompleteness, inconsistency and race conditions in formal models. The method im- plements the properties checking basing on model transitions description, and does not traverse model state space. Введение Автоматизация проверки правильности программных систем – актуальная задача современной про- граммной инженерии. Ввиду известных проблем с проверкой достижимости (комбинаторный взрыв, алго- ритмическая разрешимость), актуальны методы статической проверки [1], т. е. методы анализа переходов модели без порождения пространства ее состояний. Обнаруженная такими методами ошибка может не быть проблемой ввиду ее недостижимости, но, с другой стороны, отсутствие обнаруженных ошибок будет озна- чать их отсутствие и в пространстве достижимых состояний. В качестве примеров удачных применений по- добных методов в индустрии можно привести такие системы, как klocwork [2], FastTrack [3], Relay [4]. Суще- ствующие системы автоматической проверки программ опираются на структуру описания проверяемого ко- да, в частности, интенсивно используют структуру потока управления; явно указанная иерархия структур данных и область видимости переменных позволяет эффективнее строить отношения информационной зави- симости и т.д. Особенность предлагаемого в данной работе метода состоит в том, что он работает с множе- ством отдельных переходов, на которых изначально не определен порядок выполнения (поток управления задан «неявно» атрибутами модели или отсутствует как таковой вообще), а структура модели не всегда поз- воляет однозначно выделить модули и процессы (все атрибуты модели могут быть «глобальными»). Такая ситуация характерна на начальных стадиях проектирования и разработки программного обеспечения – на этапах формализации требований, построения абстрактных прототипов. Данная работа расширяет методы, описанные в работах [5–7], в которых предложены алгоритмы проверки полноты и непротиворечивости переходов. Далее описана формальная модель, определения проверя- емых свойств, после чего описаны методы проверки и усовершенствования в них. Формальная модель и проверяемые свойства Проверяемая модель рассматривается как транзиционная система .,,,  TPAS Здесь S – множество состояний системы, A – множество атрибутов, P – множество процессов, T – множество переходов, параметризированных идентификатором процесса. Каждое состояние из множества S представляет собой набор значений всех атрибутов из множества A . Процессы работают параллельно асинхронно и модифицируют состояния системы совершая переходы из T . Переходы являются двойками пред- и постусловий: )),,(),,(( xRpxRpx   . Предусловие ),,( xRp – формула базового языка (обычно, исчисление предикатов первого порядка). Постуловие ),,( xRp – набор присваиваний вида ),(: xRfri  , где f так же является формулой базового язы- ка. Здесь p – идентификатор процесса, совершающего данный переход, R – множество атрибутов ( RrAR i  , ), x – множество параметров перехода кроме p . Противоречивость требований – распространенная ошибка моделей поведения систем. Например, требо- вания Т1:«если в буфер 1 пришел сигнал A , необходимо вызвать процедуру X » и Т2: «если в буфер 2 пришел сигнал Term, необходимо завершить работу» противоречивы, так как допускают неоднозначность при ситуа- ции, когда оба сигнала пришли в соответствующие буферы одновременно – согласно требованию Т1 нужно выполнять процедуру X , но по требованию Т2 – завершить работу. mailto:kolchin_av@yahoo.com mailto:Stepan.Potiyenko@iss.org.ua mailto:Stepan.Potiyenko@iss.org.ua Формальні методи програмування 147 Непротиворечивость в [5] формально определяется отсутствием пересечений предусловий переходов одного процесса. Определение 1. Два перехода u и v процесса p непротиворечивы, если следующая формула общезна- чима: )),,(),,(( yRpyxRpx vvuu   . Здесь u и v – формулы предусловий, p – идентификатор процесса. Упрощенно: )( vu   . Для доказательства непротиворечивости (детерминированности) в поведении процесса достаточно проверить все пары его переходов. В работе [5] полнота определяется как общезначимость дизъюнкции предусловий всех переходов одного процесса. Определение 2. Множество переходов процесса p полно, если следующая формула общезначима:  ),,(),,( 22221111 xRpxxRpx  Здесь i – формулы предусловий, iR – наборы атрибутов, ix – наборы параметров. Упрощенно:  21  Это означает, что в данной точке потока управления всегда возможен переход. Если выполняется условие полноты, то в каждом состоянии система может совершить хотя бы один переход. Таким образом в полной системе отсутствуют тупики. Работы [5–7] при проверке полноты и непротиворечивости опираются на заданную пользователем структуру проверяемой системы. В частности, предполагается, что у каждого процесса есть специальный атрибут state (как правило, задающий поток управления), который во всех состояниях имеет конкретное значе- ние и сравнивается с конкретным значением в каждом предусловии. Это ограничение использовалось для раз- биения множества переходов на соответствующие подмножества при проверках свойств: полнота проверялась отдельно для каждого процесса, причем на подмножестве переходов, которое строится по принципу сравнения атрибута state с одинаковыми значениями; аналогично, непротиворечивость проверялась на парах переходов из одного подмножества. Далее рассмотрены примеры свойств и проблемы их проверки на моделях разных стилей формализации, в частности, без упомянутых ограничений. Метод проверки противоречивости При проверке промышленных программных систем определение 1 непротиворечивости оказалось не практичным: в императивных языках выбор очередного выполняемого оператора внутри одного процесса все- гда однозначен, т. е. такие модели детерминированы по построению. С другой стороны, даже при детерминиро- ванности всех процессов системы могут возникать патологии, связанные с параллельностью, например, колли- зии при обращении к общей памяти. Рассмотрим пример 1 Переход u процесса p1. Предусловие: p1.state = writing  x > 0 Постусловие: p1.state := idle; shared_attr := x Переход v процесса p2. Предусловие: p2.state = sending Постусловие: p2.state := ready; shared_attr := 0 Приведенные два перехода показывают пример гонки. В зависимости от последовательности их выполнения, атрибут shared_attr недетерминированно примет разные значения, однако проблем с противоре- чивостью не обнаружено, так как процессы p1 и p2, согласно определению 1, непротиворечивы (переходы будут в разных подмножествах ввиду принадлежности различным процессам). Более того, изменение струк- туры формализации может привести к обнаружению большого множества противоречивых переходов, не- смотря на неизменность поведения модели (см. примеры 2, а и 2, б). Пример 2, а. Модульная формализация Пример 2, б. Формализация на глобальных атрибутах Предусловие u: p1.state = writing  x > 0 Предусловие t: p1.state = writing  x  0 Предусловие v: p2.state = sending Предусловие u’: state_of_p1 = writing  x > 0 Предусловие t’: state_of_p1 = writing  x  0 Предусловие v’: state_of_p2 = sending В примере 2, а противоречий нет, тогда как в измененной структуре (атрибут state процесса p1 заменен глобальным state_of_p1, а процесса p2 соответственно на state_of_p2) будут обнаружены противоречия («лож- ные» с точки зрения исходной модели) между парами переходов u’ и v’ а так же t’ и v’, хотя модели находятся в трассовой эквивалентности. Таким образом, можно резюмировать описанные выше проблемы: Формальні методи програмування 148  противоречивость определена как недетерминизм одного процесса; такое определение не позволяет выявлять гонки в параллельных процессах (пример 1).  «ложная» противоречивость может возникнуть при изменении структурного описания модели, при- чем без изменения ее поведения (примеры 2, а, 2, б). Усовершенствование метода поиска противоречий Гонки в параллельных процессах (race condition) – распространенная, сложно диагностируемая потенци- альная патология распределенных систем [3, 4, 8]. Трудности в ее устранении начинаются на стадии проявле- ния – такие ошибки не всегда воспроизводимы, т.к. зависят от скорости выполнения процессов. Большая трудо- емкость устранения дефектов, возникающих из-за гонок, стимулирует развитие автоматических методов их локализации. Ввиду высокой алгоритмической сложности [9] их выявление особенно актуально для статиче- ского анализа [3, 4]. Гонки различают на такие типы: 1) write-write. Это случай, когда два процесса параллельно пишут различные значения одному атрибуту, при этом конечный результат зависит от очередности выполнения. 2) write-read. Это случай, когда один процесс присваивает значение некоторому атрибуту, в то время как другой процесс читает значение этого атрибута при осуществлении своего перехода, при этом конечный ре- зультат зависит от очередности выполнения. Теперь уточним понятие непротиворечивости. Для этого будем рассматривать переходы противоречивы- ми тогда, когда они не только недетерминированы, но при этом либо пересекаются множества атрибутов, зна- чения которых меняются в их постусловиях (write-write race condition), либо один переход изменяет значения атрибутов, которые читает в предусловии другой переход (write-read race condition). Обозначим через W(t) мно- жество атрибутов из левых частей присваиваний перехода t, а через R(t) – множество атрибутов, входящих в правые части присваиваний или в предусловие перехода t. Определение 3. Если для двух переходов u и v выполнима формула vuvWuW  ))()((  , то они находятся в отношении write-write противоречия. Определение 4. Если для двух переходов u и v выполнима формула vuvWuR  ))()((  , то они находятся в отношении write-read противоречия. Поскольку вычисление пересечения множества атрибутов эффективнее доказательства недетерминиро- ванности переходов, проверку следует начинать с построения множеств W, R. Для усиления строгости проверки противоречий можно, в случае их обнаружения, дополнительно прове- рить, что  ))),,(()),,((( uvvuvuvu ptptptpt  )),,(()),,(( uvvuvuvu ptptptpt   . Здесь ),( tspt  – предикатный трансформер системы VRS [10], преобразующий состояние s с помощью постусловия t перехода t. Приведем пример работы усовершенствованного метода. Пример 3, а: Переход u Предусловие: state = writing  x > 0 Постусловие: state := idle; shared_attr := x Переход v Предусловие: state = sending  shared_attr < 0 Постусловие: state := ready; shared_attr := 0 Несмотря на то, что оба перехода присваивают атрибуту shared_attr различные значения, здесь нет write- write гонки, т.к. переходы детерминированы – в предусловии проверяется общий атрибут state. Пример 3, б: Переход u Предусловие: state_of_p1 = writing  x > 0 Постусловие: state_of_p1 := idle; shared_attr := x Переход v Предусловие: state_of_p2 = sending  x < 2 Постусловие: state_of_p2 := ready; shared_attr := 1 Согласно определению 3, в этом примере есть write-write гонка. Однако, более строгая проверка обнару- жит, что обе последовательности (когда они возможны) выполнения – u;v и v;u – приведут к одному и тому же значению атрибута shared_attr, так как единственное значение x, допускающее одновременное выполнение пе- реходов – 1. Пример 3, в: Переход u Предусловие: p1.state = init  x > 0 Постусловие: p1.state := start; y := x Переход v Предусловие: p2.state = waiting  y < x Постусловие: p2.state := ready Формальні методи програмування 149 Пример показывает наличие write-read гонки: переход u записывает значение атрибута y, которое в свою очередь читает в предусловии переход v. Отметим так же, что переходы u и v из примера 1, согласно усовершенствованному методу, будут нахо- диться в отношении write-write гонки. Метод проверки полноты Практика использования метода, описанного в [5–7], выявила определенные недостатки: с одной сто- роны построение формализации было затруднено указанными ограничениями на использование атрибута state, с другой стороны, разбиение переходов на подмножества осуществлялось только на основании этого атрибута. Для пользователей в ряде случаев такие ограничения оказались слишком жесткими. Например, для моделирования прерываний, нужно было вообще не задавать никакого значения state в предусловии. В др у- гом случае возникла потребность изменить атрибуты state разных процессов в одном постусловии. Это за- ставляло отказываться от его использования (везде задавалось одно значение) и использовать для задания порядка выполнения обычный атрибут, не имеющий синтаксических ограничений. Это привело к фактиче- скому отсутствию разбиения переходов на подмножества, таким образом, в формулу полноты стали попадать предусловия всех переходов модели (см. примеры 4, а и 4, б). А так как промышленные системы содержат большое количество переходов (сотни и даже тысячи), возникли существенные затруднения как при доказа- тельствах больших формул, так и при их анализе. Пример 4, а. Модульная формализация Пример 4, б. Формализация на глобальных атрибутах Предусловие u: p1.state = st1  x > 0 Предусловие t: p1.state = st1  x < 0 Предусловие v: p1.state = st2  x = 0 Предусловие u’: state_of_p1 = st1  x > 0 Предусловие t’: state_of_p1 = st1  x < 0 Предусловие v’: state_of_p1 = st2  x = 0 Вердикт о неполноте: State st1: x=0 State st2:  (x=0) Вердикт о неполноте: state_of_p1=st1  x=0   state_of_p2=st1   (x = 0) Как видно, формула неполноты теперь не разбита на подформулы, ее запись соответственно увеличилась; в больших примерах из-за отсутствия разбиения формула становится чрезмерно громоздкой и вердикт стано- вится практически нечитаемым. Другая проблема возникает при использовании техники так называемого «вотч-дога» (watch-dog). Такая техника часто применяется для устранения проблем с зацикливанием, причину которого так и не удалось уста- новить. Пример 5, а. Модульная формализация Пример 5, б. Формализация на глобальных атрибутах* Предусловие u: p1.state = idle  x > 0 Предусловие t: p1.state = idle  x < 0 Предусловие v: p2.state = idle  timer < max Предусловие w: p2.state = idle  timer  max Предусловие u’: x > 0 Предусловие t’: x < 0 Предусловие v’: timer < max Предусловие w’: timer  max Вердикт о неполноте: State st1: x=0 Вердикт о неполноте: No incompleteness * Атрибуты state исключены ввиду их избыточности (здесь они всегда равны idle) Из примера видно, что после изменения структуры формализации вердикт показывает отсутствие непол- ноты, хотя поведение модели (множество ее трасс) осталось неизменным. И хотя модель в целом не имеет до- стижимых тупиков (deadlock), процесс Process1 может зайти в локальный тупик при значении x=0 (состояние «активного тупика», livelock). Таким образом, можно резюмировать описанные выше проблемы:  слишком большая формула неполноты при отсутствии разбиения по атрибуту state (примеры 4, а, б);  проблема «вотч-дога» – им может устраниться всякая неполнота, что приводит к потере обнаружения потенциальных ошибок (примеры 5, а, б). Усовершенствование метода проверки полноты В основе усовершенствования лежит принцип разделения переходов на подмножества с целью уменьше- ния размеров анализируемых формул, а так же более строгого анализа. Итак, мы ставим перед собой две задачи: (1) не потерять возможную неполноту и (2) уменьшить размер формулы неполноты. Идея решения первой задачи такова: при построении формулы неполноты учитывать только переходы, непротиворечивые (в смысле определения 1) заданному, т. е. ),|()(   iitiii Ti t иначееслиtincompl  , Формальні методи програмування 150 где t – заданный переход, T – все множество переходов модели, i – формула предусловия i-го перехода, in- compl(t) – формула неполноты для перехода t. Это позволит исключить рассмотрение параллельных независи- мых действий, и как следствие, ужесточить проверку полноты. Отметим, что теперь в примере 5б переходы v’ и w’ не будут учитываться при проверке полноты для переходов u’ и t’ (и наоборот): incompl(u’)   ((state_of_p1 = st1  x > 0)  (state_of_p1 = st1  x < 0))   (state_of_p1 = st1)  x = 0. incompl(v’)   ((timer < max)  (timer  max))  0. Заметим, что incompl(u’)  incompl(t’), а так же incompl(v’)  incompl(w’). Для решения второй проблемы предлагается ввести разбиение переходов по принципу соответствия их предусловий некоторой формуле, т. е. переход t будет рассмотрен при ограничении f если выполняется tf  . Такое ограничение может задать пользователь (например, указав, что ему интересна проверка пол- ноты при условии state_of_p1=st1), или, его можно строить автоматически, например, на основании статистиче- ских данных об использовании атрибутов в предусловиях (если поток управления задан, то он будет среди са- мых популярных). Далее представлены примеры переходов и формул неполноты; запись incompl(t, f) означает формулу неполноты для перехода t при ограничениях f. Вернемся к рассмотрению примера 4, б. В этой модели атрибут state_of_p1 часто используется, проверя- ется на равенство с различными значениями, следовательно, у него большие шансы обеспечить хорошее разби- ение. Пример 6 показывает возможные формулы неполноты для модели из примера 4, б. Пример 6. Формулы неполноты Переходы Формулы неполноты Предусловие u’: state_of_p1 = st1  x > 0 Предусловие t’: state_of_p1 = st1  x < 0 Предусловие v’: state_of_p1 = st2  x = 0 incompl(u’, state_of_p1 = st1)   (x > 0  x < 0) x = 0 incompl(t’, x < 0)   (state_of_p1 = st1) incompl(v’, state_of_p1 = st2)   (x = 0) Ниже представлены несколько дополнительных примеров, иллюстрирующих гибкость усовершенство- ванного метода. Пример 7. Гибкость усовершенствованого метода Переходы Формулы неполноты Предусловие T1: z = 1  y = 1 Предусловие T2: x = 0  a < b  y = 1 Предусловие T3: x = 0  a > b  y = 0 Предусловие T4: x = 0  a > b  y = 1 b < 0 incompl(T1, 1)  (z = 1  y = 1  x = 0  a > b  y = 0) incompl(T2, x = 0)  ( a < b  y = 1  a > b  y = 0) incompl(T3, x = 0  y = 0)  (a > b) incompl(T4, x = 0  a > b)  (y = 0  y = 1  b < 0) Выводы Описанные усовершенствования метода статической проверки полноты и непротиворечивости не чув- ствительны к изменениям структурного описания моделей, в частности, к отсутствию потока управления. Не- полнота проверяется строже, что позволяет обнаружить потенциальные ошибки, такие как активные тупики (livelock); размер формулы неполноты уменьшен за счет введения дополнительного разбиения. Проверка не- противоречивости усовершенствована возможностью обнаружения таких патологий, как гонки в параллельных вычислениях. Обнаруженные предложенным методом ошибки могут быть недостижимыми, однако отсутствие найден- ных ошибок означает их отсутствие и во множестве достижимых состояний. 1. Колчин А.В., Летичевский А.А, Потиенко С.В. и др. Обзор современных систем и методов верификации формальных моделей // Про- блеми програмування. – 2012. – № 4. – С. 59–72. 2. http://www.klocwork.com 3. Flanagan C., Freund S. FastTrack: efficient and precise dynamic race detection // ACM SIGPLAN Notices - PLDI '09. – 2009. – Vol. 44. – P. 121–133. 4. Voung J., Jhala R., Lerner S. Relay: static race detection on millions of lines of code // In Proc. of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering. – 2007. – P. 205–214. 5. Летичевский А.А. (мл.). Об одном классе базовых протоколов // Проблеми програмування. – 2005. – № 4. – С. 3–19. 6. Потиенко С.В. Статическая проверка требований и подходы к решению проблемы достижимости // Искусственный интеллект. – 2009. – № 1. – С. 192–197. 7. Potiyenko S. Static verification of basic protocols systems with unbounded number of agents // 3rd International Workshop SCSS 2010, Symbol- ic Computation in Software Science, Hagenberg, Austria, July 29-03. – 2010. – P. 51–54. 8. Naik M., Aiken A., Whaley J. Effective static race detection for Java. // Doctorial thesis, Stanford University Stanford, CA, USA. –161P. –2008. 9. Netzer R., Miller B. On the complexity of event ordering for shared-memory parallel program executions // Int. conf. On parallel processing. – 1990. – P. 1193–1197. 10. Летичевский А.А., Годлевский А.Б. и др. Свойства предикатного трансформера системы VRS // Кибернетика и системный анализ. – 2010. – № 4. – С. 3–16.

Схожі ресурси