Описан метод выявления таких патологий формальных моделей, как неполнота и противоречивость, а так же гонки в параллельных процессах. Метод реализует проверку свойств на основании анализа описания переходов модели, при этом не строит пространство ее состояний. 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. Введение Автоматизация проверки правильности программных систем - актуальная задача современной программной инженерии. Ввиду известных проблем с проверкой достижимости (комбинаторный взрыв, алгоритмическая разрешимость), актуальны методы статической проверки [1], т. е. методы анализа переходов модели без порождения пространства ее состояний. Обнаруженная такими методами ошибка может не быть проблемой ввиду ее недостижимости, но, с другой стороны, отсутствие обнаруженных ошибок будет означать их отсутствие и в пространстве достижимых состояний. В качестве примеров удачных применений подобных методов в индустрии можно привести такие системы, как klocwork [2], FastTrack [3], Relay [4]. Существующие системы автоматической проверки программ опираются на структуру описания проверяемого кода, в частности, интенсивно используют структуру потока управления; явно указанная иерархия структур данных и область видимости переменных позволяет эффективнее строить отношения информационной зависимости и т.д. Особенность предлагаемого в данной работе метода состоит в том, что он работает с множеством отдельных переходов, на которых изначально не определен порядок выполнения (поток управления задан «неявно» атрибутами модели или отсутствует как таковой вообще), а структура модели не всегда позволяет однозначно выделить модули и процессы (все атрибуты модели могут быть «глобальными»). Такая ситуация характерна на начальных стадиях проектирования и разработки программного обеспечения - на этапах формализации требований, построения абстрактных прототипов. Данная работа расширяет методы, описанные в работах [5-7], в которых предложены алгоритмы проверки полноты и непротиворечивости переходов. Далее описана формальная модель, определения проверяемых свойств, после чего описаны методы проверки и усовершенствования в них. Постуловие ( p, R, x) - набор присваиваний вида ri : f (R, x) , где f так же является формулой базового языка. Здесь p - идентификатор процесса, совершающего данный переход, R - множество атрибутов ( R A, ri R ), x - множество параметров перехода кроме p . Противоречивость требований - распространенная ошибка моделей поведения систем. Например, требования Т1:«если в буфер 1 пришел сигнал A , необходимо вызвать процедуру X » и Т2: «если в буфер 2 пришел сигнал Term, необходимо завершить работу» противоречивы, так как допускают неоднозначность при ситуации, когда оба сигнала пришли в соответствующие буферы одновременно - согласно требованию Т1
Формальная модель и проверяемые свойства Проверяемая модель рассматривается как транзиционная система
Здесь S – множество состояний системы, A – множество атрибутов, P – множество процессов, T – множество переходов, параметризированных идентификатором процесса. Каждое состояние из множества S представляет собой набор значений всех атрибутов из множества A .
Процессы работают параллельно асинхронно и модифицируют состояния системы совершая переходы из T . Переходы являются двойками пред- и постусловий: нужно выполнять процедуру X , но по требованию Т2 – завершить работу.
Непротиворечивость в [5] формально определяется отсутствием пересечений предусловий переходов одного процесса.
Определение 1. Два перехода u и v процесса p непротиворечивы, если следующая формула общезначима: Здесь u и v – формулы предусловий, p – идентификатор процесса. Упрощенно: (x u ( p, Ru , x) y v ( p, Rv , y)) .
( u v ) . x11( p, R1, x1) x2 2 ( p, R2 , x2 )
1 2 Для доказательства непротиворечивости (детерминированности) в поведении процесса достаточно проверить все пары его переходов.
В работе [5] полнота определяется как общезначимость дизъюнкции предусловий всех переходов одного процесса.
Определение 2. Множество переходов процесса p полно, если следующая формула общезначима: Здесь i – формулы предусловий, Ri – наборы атрибутов, xi – наборы параметров. Упрощенно: Это означает, что в данной точке потока управления всегда возможен переход. Если выполняется условие полноты, то в каждом состоянии система может совершить хотя бы один переход. Таким образом в полной системе отсутствуют тупики.
Работы [
При проверке промышленных программных систем определение 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, а. Модульная формализация Предусловие u: p1.state = writing x > 0 Предусловие t: p1.state = writing x 0 Предусловие v: p2.state = sending Пример 2, б. Формализация на глобальных атрибутах Предусловие 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’, хотя модели находятся в трассовой эквивалентности.
Таким образом, можно резюмировать описанные выше проблемы: противоречивость определена как недетерминизм одного процесса; такое определение не позволяет выявлять гонки в параллельных процессах (пример 1).
«ложная» противоречивость может возникнуть при изменении структурного описания модели, причем без изменения ее поведения (примеры 2, а, 2, б). Усовершенствование метода поиска противоречий
Гонки в параллельных процессах (race condition) – распространенная, сложно диагностируемая
потенциальная патология распределенных систем [
1) write-write. Это случай, когда два процесса параллельно пишут различные значения одному атрибуту, при этом конечный результат зависит от очередности выполнения.
2) write-read. Это случай, когда один процесс присваивает значение некоторому атрибуту, в то время как другой процесс читает значение этого атрибута при осуществлении своего перехода, при этом конечный результат зависит от очередности выполнения.
Теперь уточним понятие непротиворечивости. Для этого будем рассматривать переходы противоречивыми тогда, когда они не только недетерминированы, но при этом либо пересекаются множества атрибутов, значения которых меняются в их постусловиях (write-write race condition), либо один переход изменяет значения атрибутов, которые читает в предусловии другой переход (write-read race condition). Обозначим через W(t) множество атрибутов из левых частей присваиваний перехода t, а через R(t) – множество атрибутов, входящих в правые части присваиваний или в предусловие перехода t.
Определение 3. Если для двух переходов u и v выполнима формула (W (u) W (v)) u v , то они находятся в отношении write-write противоречия.
Определение 4. Если для двух переходов u и v выполнима формула (R(u) W (v)) u v EMBED, то они находятся в отношении write-read противоречия.
Поскольку вычисление пересечения множества атрибутов эффективнее доказательства недетерминированности переходов, проверку следует начинать с построения множеств W, R.
Для усиления строгости проверки противоречий можно, в случае их обнаружения, дополнительно проверить, что
( pt( pt( u v , u ), v ) pt( pt( u v , v ), u )) pt( pt( u v , u ), v ) pt( pt( u v , v ), u ) EMBED.
Здесь pt(s, t ) – предикатный трансформер системы VRS [
Приведем пример работы усовершенствованного метода. Пример 3, а: Переход u Предусловие: state = writing x > 0 Постусловие: state := idle; shared_attr := x Переход v Предусловие: state = sending shared_attr < 0 Постусловие: state := ready; shared_attr := 0 Пример 3, б:
Несмотря на то, что оба перехода присваивают атрибуту shared_attr различные значения, здесь нет writewrite гонки, т.к. переходы детерминированы – в предусловии проверяется общий атрибут state. Переход 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. Переход u Предусловие: p1.state = init x > 0 Постусловие: p1.state := start; y := x Переход v Предусловие: p2.state = waiting y < x Постусловие: p2.state := ready Пример показывает наличие write-read гонки: переход u записывает значение атрибута y, которое в свою очередь читает в предусловии переход v.
Отметим так же, что переходы u и v из примера 1, согласно усовершенствованному методу, будут находиться в отношении write-write гонки. Метод проверки полноты
Практика использования метода, описанного в [
Пример 4, а. Модульная формализация Предусловие u: p1.state = st1 x > 0 Предусловие t: p1.state = st1 x < 0 Предусловие v: p1.state = st2 x = 0 Вердикт о неполноте: State st1: x=0 State st2: (x=0) Пример 4, б. Формализация на глобальных атрибутах Предусловие u: p1.state = idle x > 0 Предусловие t: p1.state = idle x < 0 Предусловие v: p2.state = idle timer < max Предусловие w: p2.state = idle timer max Вердикт о неполноте: State st1: x=0 Пример 5, б. Формализация на глобальных атрибутах* Предусловие u’: x > 0 Предусловие t’: x < 0 Предусловие v’: timer < max Предусловие w’: timer max Вердикт о неполноте:
No incompleteness * Атрибуты state исключены ввиду их избыточности (здесь они всегда равны idle)
Из примера видно, что после изменения структуры формализации вердикт показывает отсутствие неполноты, хотя поведение модели (множество ее трасс) осталось неизменным. И хотя модель в целом не имеет достижимых тупиков (deadlock), процесс Process1 может зайти в локальный тупик при значении x=0 (состояние «активного тупика», livelock).
Таким образом, можно резюмировать описанные выше проблемы: слишком большая формула неполноты при отсутствии разбиения по атрибуту state (примеры 4, а, б); проблема «вотч-дога» – им может устраниться всякая неполнота, что приводит к потере обнаружения потенциальных ошибок (примеры 5, а, б). Усовершенствование метода проверки полноты
В основе усовершенствования лежит принцип разделения переходов на подмножества с целью уменьшения размеров анализируемых формул, а так же более строгого анализа. Итак, мы ставим перед собой две задачи: (1) не потерять возможную неполноту и (2) уменьшить размер формулы неполноты. Идея решения первой задачи такова: при построении формулы неполноты учитывать только переходы, непротиворечивые (в смысле определения 1) заданному, т. е.
incompl (t) ( t iT i | i i если t i , иначе i ) , где t – заданный переход, T – все множество переходов модели, i – формула предусловия i-го перехода, incompl(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 если выполняется f t . Такое ограничение может задать пользователь (например, указав, что ему интересна проверка полноты при условии 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); размер формулы неполноты уменьшен за счет введения дополнительного разбиения. Проверка непротиворечивости усовершенствована возможностью обнаружения таких патологий, как гонки в параллельных вычислениях.
Обнаруженные предложенным методом ошибки могут быть недостижимыми, однако отсутствие найденных ошибок означает их отсутствие и во множестве достижимых состояний.