СПОСОБ ВЕРИФИКАЦИИ ФОРМАЛЬНОЙ АВТОМАТНОЙ МОДЕЛИ ПОВЕДЕНИЯ ПРОГРАММНОЙ СИСТЕМЫ Российский патент 2019 года по МПК G06F11/00 G06N7/00 

Область техники

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

Уровень техники

В современной жизни большое значение имеет разнообразное программное обеспечение (ПО). В силу развития бизнеса и технологий управления требования к функциональности, производительности и надежности ПО постоянно возрастают, поэтому и его сложность все время растет. Для стабильного экономического и технологического развития общества необходимо, чтобы широко используемые программные системы, несмотря на их сложность, работали надежно и корректно, т.е., в соответствии с требованиями к ним. Убедиться в корректной работе ПО можно с помощью различных методов его верификации.

При верификации сложного ПО обычно необходимо заранее как можно более полно и точно описать его желательные характеристики и используемые при его разработке проектные решения. Такое описание часто фиксируется в виде моделей поведения ПО. Модели поведения очень разнообразны, довольно широко используются автоматные модели с инвариантами, далее они называются просто автоматными моделями. Такая модель состоит из четырех частей: 1) набора состояний, описываемых некоторыми внутренними данными или переменными системы, возможные комбинации значений переменных задают возможные состояния, 2) выделенного непустого множества возможных начальных состояний, может быть, включающего только одно состояние, 3) набора событий и правил, определяющих переходы между состояниями (изменения переменных) по произошедшим событиям, и 4) набора инвариантов или свойств, которые должны выполняться во всех достижимых состояниях системы. Достижимыми называются состояния, в которых система может оказаться при переходах из некоторого начального состояния в результате выполнения произвольных последовательностей событий в соответствии с описанными в модели правилами. События могут иметь параметры, значения которых задаются при выполнении (или наступлении) такого события. Правила для событий делятся на предусловия событий и постусловия событий. Предусловие события описывает в виде логического предиката ограничения на значения параметров этого события и значения переменных системы, при выполнении которых оно может происходить. Множество наборов значений переменных системы и параметров события, удовлетворяющих его предусловию, называется доменом события. Постусловие события описывает изменение значений переменных модели при наступлении данного события в зависимости от значений его параметров и значений переменных, предшествовавших наступлению события. Начальные состояния могут быть заданы прямо возможными значениями переменных в них, либо при помощи специального события инициализации, в постусловии которого описываются начальные значения переменных системы.

Для описания подобных моделей используются языки моделирования из семейства VDM: VDMSL, VDM++; RSL; Z, В, Event-B. Общий метод VDM и язык VDMSL описаны в работе [, D., Jones, С.В. The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science 61. Berlin, Heidelberg, New York: Springer, 1978.]. Язык VDM++ описан в работе Fitzgerald [Fitzgerald, J.S., Larsen, P.G. Modelling Systems: Practical Tools and Techniques in Software Engineering. Cambridge University Press, 1998.]. Язык RSL описан в работе RAISE Language Group [RAISE Language Group. The RAISE specification language. Prentice Hall, 1992.]. Основанный на развитии Z и В язык Event-В описан в работе Abrial [Abrial, J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.].

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

Одним из этапов верификации ПО, разрабатываемого с использованием подобных моделей, является верификация самих моделей - подтверждение того, что модель построена корректно. Если это не так, надеяться на создание корректно работающего ПО на основе такой модели бессмысленно. Для автоматных моделей такая верификация означает подтверждение (при помощи симуляции, статического анализа или формального математического доказательства) того, что сформулированные в рамках модели инварианты действительно выполняются во всех достижимых состояниях. Далее для конкретности изложения в описании существующего уровня техники и предлагаемого способа рассматривается верификация автоматных моделей при помощи формального математического доказательства их инвариантов.

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

Отношение между двумя моделями, уточняемой и уточненной, считается отношением уточнения, описанном в работах Abrial, и Abrial и др. [Abrial, J.-R., Hallerstede, S. Refinement, decomposition and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae, 77(1-2):1-28, 2006.], если выполнены следующие условия.

1. Переменные уточненной модели включают все переменные уточняемой и могут содержать новые переменные. Заимствованные из уточняемой модели переменные называются далее старыми переменными, все остальные переменные уточненной модели - новыми.

2. Если взять значения только старых переменных в любом начальном состоянии уточненной модели, должно получиться начальное состояние уточняемой модели (множество начальных состояний, рассматриваемое с точки зрения значений старых переменных, может только сузиться в уточненной модели).

3. События уточненной модели содержат все события уточняемой и могут включать новые события.

4. Правила, описывающие изменения переменных при наступлении событий либо сохраняются, либо расширяются следующим образом.

a. Предусловия событий, имеющихся в уточняемой модели, в уточненной могут сохраняться или усиливаться (т.е., из предусловия события уточненной модели должно следовать предусловие соответствующего события уточняемой модели).

b. Постусловия событий, имеющихся в уточняемой модели, в уточненной могут быть пополнены правилами изменения новых переменных. Старые переменные должны меняться в точности по тем же правилам, что и в уточняемой модели.

c. Постусловия новых событий уточненной модели могут описывать только изменения новых переменных.

Если уточнение построено корректно (выполняются указанные ограничения на отношение между двумя моделями), то инварианты, верные для уточняемой модели, будут верны и для уточненной модели. Соответственно, их можно не проверять, если доказана корректность уточнения, сэкономив тем самым усилия на проверку корректности уточненной модели.

Верификация с использованием отношения уточнения выполняется с помощью следующих шагов, описанных в работах Abrial и Abrial и др.

1) Определяется более простая модель, чья корректность может быть проверена с существенно меньшими трудозатратами.

a. Либо эта модель берется в готовом виде из имеющихся наработок и публикаций.

b. Либо она строится следующим способом.

Выделяется подмножество переменных верифицируемой модели так, чтобы часть ее событий изменяла только переменные, не входящие в это подмножество (остальные события могут менять и переменные из этого подмножества и все остальные). Создается более простая автоматная модель, переменные которой совпадают с выделенным подмножеством переменных исходной верифицируемой модели, события совпадают с подмножеством всех событий исходной модели, которые могут менять переменные из выделенного подмножества, а инварианты являются подмножеством инвариантов верифицируемой модели, зависящим только от переменных выделенного подмножества. Начальными состояниями простой модели объявляются комбинации значений переменных, соответствующие начальным состояниям верифицируемой модели.

2) Выполняется проверка того, что простая модель и верифицируемая модель находятся в отношении уточнения, описанном выше.

3) Простая модель верифицируется, проверяется выполнение ее инвариантов (при помощи математического доказательства).

4) Проверяется (при помощи математического доказательства) выполнение инвариантов верифицируемой модели в ее начальном состоянии.

5) Проверяется (при помощи математического доказательства) выполнение во всех состояниях инвариантов верифицируемой модели, не входящих в множество инвариантов простой модели.

Описанный традиционный подход к верификации формальных моделей с использованием уточнения применим, если возможно построение прямого соответствия между событиями верифицируемой и более простой моделей. При анализе моделей сложных программных систем такое соответствие часто не может быть построено, в этих случаях, несмотря на то, что более простая и верифицируемая модели похожи и имеют практически совпадающие наборы инвариантов, корректность верифицируемой модели приходится доказывать полностью заново, во многом повторяя доказательства тех инвариантов, которые совпадают с инвариантами простой модели. Это особенно характерно для ситуаций, в которых упрощенная модель описывает важные свойства системы с точки зрения определенного аспекта (защищенности, корректности, производительности), используя только некоторые базовые операции в качестве событий, а более сложная верифицируемая модель предназначена для описания тех же свойств, но использует в качестве интерфейса системы более богатый и сложный набор операций, которые не отображаются на базовые прямо. В этих ситуациях упрощенная модель, определяемая на первом шаге описанного метода, оказывается все еще слишком сложной для эффективного анализа и проведения верификации, т.е., выполнение третьего шага оказывается слишком трудоемко.

Еще острее проблема определения прямого соответствия между событиями моделей проявляется при верификации сложной модели в пошаговой манере, с помощью нескольких шагов упрощения. В такой ситуации даже эти несколько шагов часто не дают возможности упростить модель достаточно для эффективного проведения доказательства инвариантов, поскольку набор событий самой простой модели должен сохраняться на каждом шаге уточнения и входить неизменным в набор событий самой сложной модели.

Решаемая техническая задача

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

Сущность изобретения

Для решения технической задачи предлагается способ верификации формальной автоматной модели поведения программной системы, сущность которого состоит в использовании более простой автоматной модели, для которой инварианты являются подмножеством инвариантов верифицируемой модели, переменные являются подмножеством переменных верифицируемой модели, и каждое событие верифицируемой формальной автоматной модели либо определяет изменение только не входящих в более простую автоматную модель переменных и называется вспомогательным, либо эквивалентно выполнению цепочки из вспомогательных событий и событий более простой автоматной модели, причем выбор такой цепочки однозначно определяется значениями параметров события и переменных верифицируемой формальной автоматной модели, при этом для верификации вначале проверяют, что предусловие каждого события в каждой цепочке, эквивалентной событию верифицируемой модели, следует из постусловий предыдущих событий в этой же цепочке и исходных ограничений на значения параметров события и переменных верифицируемой модели, и что совместное постусловие событий в каждой цепочке влечет постусловие соответствующего этой цепочке события верифицируемой модели, затем проверяют выполнение инвариантов более простой автоматной модели во всех ее состояниях, затем проверяют выполнение инвариантов верифицируемой формальной автоматной модели в ее начальных состояниях, затем проверяют выполнение во всех состояниях инвариантов верифицируемой формальной автоматной модели, не входящих в простую модель и по результатам проверок делают заключение о корректности верифицируемой модели.

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

Кроме того, более простую автоматную модель могут выбирать из уже существующих.

Предлагаемое изобретение и его работа поясняются графическими материалами, представленными на Фиг. 1 и Фиг. 2.

На Фиг. 1 представлена схема действия open для несуществующих и существующих файлов.

На Фиг. 2 представлен полный граф расширенного уточнения события open. На нем события уточненной модели изображены прямоугольниками; если событие вспомогательное, в прямоугольнике показано только его имя, если же событие соответствует уточняемому, то в его прямоугольнике снизу показано имя уточняемого события МРОСЛ ДП-модели.

Для пояснения того, как работает предлагаемый способ верификации формальной автоматной модели поведения программной системы, введем правила отношения расширенного уточнения между моделями.

Эти правила состоят в том, что две модели, уточняемая и уточненная, находятся в отношении расширенного уточнения, если они удовлетворяют следующим условиям.

1. Переменные уточненной модели включают все переменные уточняемой и могут содержать новые переменные. Заимствованные из уточняемой модели переменные называются далее старыми переменными, все остальные переменные уточненной модели - новыми.

2. Если взять значения только старых переменных в любом начальном состоянии уточненной модели, должно получиться начальное состояние уточняемой модели (множество начальных состояний, рассматриваемое с точки зрения значений старых переменных, может только сузиться в уточненной модели).

3. События уточненной модели делятся на два типа: уточненные события (они связаны с событиями уточняемой модели, но не прямо, они не обязаны присутствовать в ней, как в случае обычного уточнения) и вспомогательные события.

4. Для каждого вспомогательного события выполнено следующее.

a. Предусловия вспомогательных событий могут задавать любые ограничения.

b. Постусловия вспомогательных событий могут задавать изменения только новых переменных.

5. Для каждого уточненного события выполнено следующее.

a. Домен события разбит на конечное семейство множеств, каждому элементу которого сопоставлена конечная последовательность из событий уточняемой модели и вспомогательных событий. Каждый такой элемент выделяется определенным условием на значения параметров уточненного события и значения переменных модели, предшествующие его наступлению. Элементы заданного так семейства множеств называются субдоменами события. Последовательность событий, сопоставленная субдомену, называется связанной с ним цепочкой.

b. Предусловие уточненного события формулируется так, чтобы в каждом субдомене (при выполнении соответствующих ему ограничений) гарантировать выполнение предусловий всех событий в соответствующей цепочке. Т.е., само предусловие вместе с ограничением субдомена должно влечь выполнение предусловия первого события в соответствующей субдомену цепочке, изменения в соответствии с постусловием первого события должны влечь выполнение предусловия второго в цепочке события, и т.д., каждый раз изменения в соответствии с постусловием очередного события в цепочке вместе с предшествующими ему предусловиями должны влечь выполнение предусловия следующего события цепочки.

с. В постусловии уточненного события в рамках каждого субдомена правила изменения переменных уточненной модели соответствуют композиции правил изменения переменных из постусловий событий, участвующих в связанной с данным субдоменом цепочке (т.е., переменные модели меняются так, как если бы вместо данного события выполнялась связанная цепочка из событий уточняемой модели, изменяющих значения старых переменных, и вспомогательных событий, изменяющих значения новых переменных).

При этом следует иметь в виду, что семейство субдоменов и связанных с ними цепочек из правила 5.а может быть не конечным (конечное множество субдоменов и конечная цепочка, связанная с каждым из них), а финитным. Это означает, что есть эффективное разбиение домена на субдомены и эффективное построение цепочек, т.е., задана алгоритмическая процедура, позволяющая по значениям параметров уточненного события и переменных модели определить номер соответствующего субдомена и соответствующую конечную цепочку вспомогательных событий и событий уточняемой модели. Общая длина таких цепочек может быть не ограничена, но каждая конкретная цепочка конечна. Общее число субдоменов при этом также может быть бесконечно, но они считаются занумерованными натуральными числами.

Работа предлагаемого способа верификации формальной автоматной модели поведения программной системы состоит из следующих шагов.

1) Определяют более простую модель, корректность которой может быть проверена с существенно меньшими трудозатратами.

a. Либо эту модель берут в готовом виде из имеющихся наработок и публикаций.

b. Либо ее строят следующим способом.

Выделяют подмножество переменных верифицируемой модели так, чтобы часть ее событий изменяла только переменные, не входящие в это подмножество. Создают более простую автоматную модель, переменные которой совпадают с выделенным подмножеством переменных исходной верифицируемой модели, а инварианты являются подмножеством инвариантов верифицируемой модели, зависящим только от переменных выделенного подмножества. Начальными состояниями простой модели объявляют комбинации значений переменных, соответствующие начальным состояниям верифицируемой модели. События исходной модели, которые могут менять переменные из выделенного подмножества, разбивают на более простые действия, одна часть которых совпадает с событиями, меняющими переменные, не входящие в выделенное подмножество, а вторая часть меняет только переменные, входящие в выделенное множество, и эту вторую часть событий объявляют событиями простой модели.

2) Выполняют проверку того, что построенная простая модель и верифицируемая модель находятся в отношении расширенного уточнения, описанном выше.

3) Простую модель верифицируют, проверяют выполнение ее инвариантов (при помощи математического доказательства).

4) Проверяют (при помощи математического доказательства) выполнение инвариантов верифицируемой модели в ее начальном состоянии.

5) Проверяют (при помощи математического доказательства) выполнение во всех состояниях инвариантов верифицируемой модели, не входящих в множество инвариантов простой модели.

При наличии отношения расширенного уточнения между моделями и выполнении инвариантов уточняемой модели в начальном состоянии уточненной модели, инварианты уточняемой модели также выполняются во всех состояниях уточненной модели. Это так, поскольку любое достижимое состояние модели достигается при выполнении конечной цепочки ее событий. Такие события в уточненной модели по построению расширенного уточнения (правило 3) могут быть либо вспомогательными, либо уточненными. Выполнение вспомогательных событий по построению расширенного уточнения (правило 4) не меняет значений старых переменных, а значит, не изменяет выполнения этих инвариантов (они зависят только от старых переменных). Выполнение уточненного события по построению расширенного уточнения (правило 5.с) изменяет переменные модели эквивалентно некоторой цепочке из вспомогательных событий и событий уточняемой модели. При этом правило 5.b гарантирует выполнение предусловий всех событий в цепочке. Вспомогательные события, как уже показано, не меняют выполнения инвариантов. События уточняемой модели также не меняют выполнения инвариантов, поскольку инварианты уточняемой модели считаются выполненными. Таким образом, при достижении любого состояния из начального по некоторой цепочке событий уточненной модели, выполнение инвариантов не меняется при выполнении каждого события этой цепочки, и, раз они выполнены в начальном состоянии, то должны быть выполнены и в конечном.

Согласно сказанному, после выполнения шага 5 предлагаемого способа можно считать доказанными все инварианты верифицируемой модели, не тратя усилий на доказательство инвариантов, входящих в простую модель.

Для упрощения работы с набором цепочек событий, эквивалентных одному уточненному событию в разных ситуациях, этот набор может описываться в виде конечного размеченного графа с выделенной начальной вершиной, каждое ребро которого помечается условием срабатывания этого ребра и либо вспомогательным событием, либо событием уточняемой модели. В этом случае процедура построения цепочки, соответствующей заданным значениям параметров и переменных, выглядит как выполнение последовательности проходов из начальной вершины графа по тем его ребрам, для которых на данный момент выполнено условие срабатывания (с учетом ранее выполненных в результате срабатывания событий изменений переменных), и последовательное увеличение строящейся цепочки событиями, помечающими проходимые при этой процедуре ребра.

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

Технический результат достигается за счет использования при верификации автоматных моделей отношения расширенного уточнения между моделями, устанавливающее контекстно-зависимое цепное соответствие между событиями верифицируемой модели и событиями более простой (эталонной) модели, в соответствии с которым каждому уточненному событию верифицируемой модели сопоставляют семейства конечных последовательностей из вспомогательных событий и событий более простой (эталонной) модели.

Конкретный пример, иллюстрирующий работу изобретения

Верифицируемая модель

Верифицируемая модель представляет собой описание механизмов защиты данных файловой системы операционной системы Linux от несанкционированного доступа в терминах ролей, уровней доступа, конфиденциальности и целостности.

Переменными данной модели являются сущности, сессии, роли, учетные записи пользователей, доступы, права доступа, а также различные метки и флаги. Сущности представляют те объекты операционной системы, к которым назначаются и контролируются права доступа, например, файлы и каталоги. Роли являются контейнерами прав доступа к сущностям и к другим ролям. Сессии - это процессы операционной системы, каждый из них функционирует от имени соответствующей учетной записи пользователя. При условии, что сессия обладает доступом к роли, у которой есть право доступа к сущности, она может получить доступ на чтение или запись к этой сущности.

Каждой сессии и каждой сущности приписаны уровни целостности и конфиденциальности. Уровни целостности линейно упорядочены. Уровни конфиденциальности упорядочены частично, образуя решетку (т.е., для любых двух уровней конфиденциальности есть наибольший уровень, меньший их обоих, и наименьший уровень, больший их обоих).

Кроме того, переменные верифицируемой модели также включают некоторые данные ядра операционной системы, например, файловые дескрипторы, идентификаторы задач, сокеты и пр.

Ограничения на доступы сессий к сущностям и ролям в модели основаны на трех механизмах защиты информации: мандатный контроль целостности, мандатное управление доступом, управление доступом на основе ролей. Данные ограничения описываются в виде инвариантов.

Инвариант, описывающий ограничение доступа на основе ролей, выглядит так: сессия может иметь доступ на чтение или запись к сущности только, если у этой сессии есть доступ к роли с правом на чтение или запись к данной сущности.

Инвариант, описывающий ограничение доступа на основе контроля целостности, выглядит так: сессия может иметь доступ на запись к сущности только, если уровень целостности, приписанный этой сессии, больше или равен уровня целостности, приписанного данной сущности.

Инварианты, описывающие ограничение доступа на основе контроля конфиденциальности, выглядят так: сессия может иметь доступ на чтение к сущности только, если уровень конфиденциальности этой сессии больше или равен уровня конфиденциальности данной сущности. Сессия может иметь доступ на запись к сущности только, если уровень конфиденциальности этой сессии равен уровня конфиденциальности данной сущности.

Набор инвариантов также включает ограничения, описывающие корректность построения данных ядра и их связи с абстрактными данными, например, соответствие между сущностями и дескрипторами файлов.

Событиями верифицируемой модели являются системные вызовы ядра операционной системы. Примерами системных вызовов служат функция открытия файла open, функция чтения открытого файла read, функция записи в открытый файл write.

Построение уточняемой модели

Для облегчения верификации модели полезно разделить верификацию инвариантов, описывающих ограничения доступа, и инвариантов, описывающих ограничения целостности данных ядра.

В данном примере использована описанная в работе Девянин и др. [Девянин П.Н., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. О представлении МРОСЛ ДП-модели в формализованной нотации Event-B. Проблемы информационной безопасности. Компьютерные системы, 2014(3):7-15.] упрощенная МРОСЛ ДП-модель (мандатная сущностно-ролевая модель с учетом потоков данных), подходящая для анализа свойств информационной безопасности. Ее переменными являются только абстрактные данные, включающие сессии, сущности, доступы сессий к сущностям, роли, уровни целостности и конфиденциальности, но не включающие их способы реализации в ядре операционной системы. Инвариантами упрощенной модели являются только инварианты, касающиеся ограничений доступа.

Чтобы добиться желаемого упрощения, среди системных вызовов выделяются вспомогательные действия, оперирующие только с данными ядра. Остальные системные вызовы мы будем пытаться представить в виде композиции вспомогательных действий и абстрактных операций, производящих изменения абстрактных переменных упрощенной модели. Эти абстрактные операции дальше являются событиями упрощенной модели.

При этом упрощенная модель оказывается уточняемой, а исходная - уточненной в рамках отношения расширенного уточнения, определенного выше.

Пример определения расширенного уточнения для операции open

Рассмотрим пример системного вызова open, который является событием уточненной модели, это событие представлено функцией int open(const char *pathname, int flags), которая выполняет действия, необходимые для открытия файла.

У операции open два параметра: строка pathname содержит путь до открываемого файла, a flags определяет вид доступа, который требуется получить - на чтение, на запись, или на чтение и на запись одновременно. За это отвечают флаги O_RDONLY, O_WRONLY, O_RDWR. flags также может содержать дополнительные, необязательные флаги. Функция возвращает ассоциированный с файлом файловый дескриптор, который затем может использоваться в последующих системных вызовах (например, в read, write, lseek, fcntl).

Файл с именем pathname, файловый дескриптор которого требуется получить, может существовать или отсутствовать в файловой системе. Если файл не существует, а в параметре flags установлен дополнительный флаг O_CREAT, то в ходе работы open он будет создан. В виде графа соответствующие данным субдоменам open цепочки событий будут выглядеть так, как показано на Фиг. 1.

Если рассмотреть домен уточненного события целиком, то соответствующий граф из событий будет гораздо более ветвистым.

В соответствии с предлагаемым способом, узлы графов системных вызовов, которые соответствуют событиям упрощенной модели (узел создания файла в open является событием создания объекта create_object в упрощенной модели), будут представлены в уточненной модели как уточнения этих событий. Оставшиеся вспомогательные события (такие как разбор параметров pathname и flags системного вызова open) будут представлены как вспомогательные события, изменяющие исключительно состояние уточненной модели. Используя средства языка моделирования, данные события затем будут объединены в виде цепочки.

Рассмотрим субдомен уточненного события open, при котором файл из параметра pathname не существует, а параметр flags содержит флаг O_WRONLY, что означает открытие файла на запись, и дополнительный флаг O_CREAT, что позволит создать файл. Если процесс, от имени которого вызывается open, обладает всеми нужными доступами и правами доступа, то этому случаю будет соответствовать цепочка из семи событий, представляющая субдомен уточненного события open: open_start=>open_check_p=>open_create=>open_check=>open_grant_write=>open_write=>open_finish где:

- В событии open_start находятся предусловия, которые описывают рассматриваемый частный случай (случай, когда файл, который требуется открыть, еще не существует);

- В событии open_check_p принимается решение, какое событие должно произойти следующим. Так как в данном случае все требуемые для создания файла доступы и права доступа имеются, то следующим событием будет open_create;

- Событие open_create является уточнением события create_object из упрощенной модели, которое описывает создание нового объекта (файла);

- В событии open_check принимается решение, какое событие должно произойти следующим. В данном случае для получения доступа на запись к созданному файлу требуется получить право доступа на запись к нему, следовательно, следующим событием будет open_grant_write;

- Событие open_grant_write является уточнением события grant_rights упрощенной модели, которое описывает получение права доступа на запись;

- Событие open_write является уточнением события access_write упрощенной модели, которое описывает получение доступа на запись;

- Событие open_finish в своем постусловии возвращает запрашиваемый файловый дескриптор.

Данная цепочка событий соответствует субдомену уточненного события open. При применении предлагаемого способа кроме данного субдомена были описаны еще несколько (итоговый граф показан на Фиг. 2, на нем события уточненной модели изображены прямоугольниками; если событие вспомогательное, в прямоугольнике показано только его имя, если же событие соответствует уточняемому, то в его прямоугольнике снизу показано имя уточняемого события МРОСЛ ДП-модели). Если таким образом описать все оставшиеся субдомены, то полученный граф будет являться представлением уточненного события, а проведенные доказательства подтвердят соответствие с операциями уточняемой модели, что в свою очередь будет означать, что уточненное событие сохраняет все установленные в уточняемой модели инварианты.

Завершение верификации модели

Описанная в предыдущем разделе процедура построения цепочек уточняющих операций, объединяемых в граф, выполняется для всех событий верифицируемой модели. В итоге выделяется набор событий, которые являются вспомогательными и не изменяют переменные, соответствующие абстрактным данным, и набор абстрактных событий, изменяющих только абстрактные данные. Абстрактные события объявляются событиями упрощенной модели. Способ их выделения определяет субдомены и цепочки событий, соответствующие субдоменам.

Для выполнения шага 2 предложенного способа - проверки расширенного уточнения - необходимо проверить выполнение пунктов 5.b и 5.c правила. В данном примере эта проверка выполняется в виде проведения математического доказательства.

Шаги 3, 4 и 5 предложенного способа требуют выполнения проверки, соответственно, инвариантов упрощенной модели, инвариантов исходной модели в ее начальном состоянии и тех инвариантов исходной модели, которые не были перенесены в упрощенную модель. В данном примере эта проверка возможна в виде проведения математических доказательств и выполняется с помощью инструмента интерактивного построения доказательств.

Изобретение относится к способу верификации формальной автоматной модели поведения программной системы. Технический результат заключается в автоматизации проверки корректности верифицируемой автоматной модели. В способе при построении более простой автоматной модели выделяют подмножество переменных верифицируемой формальной автоматной модели так, чтобы часть ее событий изменяла только переменные, не входящие в это подмножество, используют переменные, инварианты и начальные состояния более простой автоматной модели, разбивают события верифицируемой формальной автоматной модели на цепочки более простых действий, проверяют предусловия и постусловия событий в каждой цепочке, проверяют выполнение инвариантов более простой автоматной модели во всех ее состояниях, проверяют выполнение инвариантов верифицируемой формальной автоматной модели в ее начальных состояниях, проверяют выполнение во всех состояниях инвариантов верифицируемой формальной автоматной модели, не входящих в простую модель, и по результатам проверок делают заключение о корректности верифицируемой модели. 1 з.п. ф-лы, 2 ил.

1. Способ верификации формальной автоматной модели поведения программной системы, включающий использование более простой автоматной модели, для чего строят более простую автоматную модель, при этом выделяют подмножество переменных верифицируемой формальной автоматной модели так, чтобы часть ее событий изменяла только переменные, не входящие в это подмножество, переменными более простой автоматной модели объявляют выделенное подмножество переменных верифицируемой формальной автоматной модели, инвариантами более простой автоматной модели объявляют подмножество инвариантов верифицируемой формальной автоматной модели, зависящих только от переменных выделенного подмножества, начальными состояниями более простой автоматной модели объявляют комбинации значений ее переменных, соответствующие начальным состояниям верифицируемой формальной автоматной модели, события верифицируемой формальной автоматной модели, которые могут менять переменные из выделенного подмножества, разбивают на цепочки более простых действий, одна часть которых совпадает с событиями, меняющими переменные, не входящие в выделенное подмножество, а вторая часть меняет только переменные, входящие в выделенное множество, и событиями более простой автоматной модели объявляют действия, входящие в эту вторую часть, при этом в процессе верификации вначале проверяют, что предусловие каждого события в каждой цепочке, эквивалентной событию верифицируемой модели, следует из постусловий предыдущих событий в этой же цепочке и исходных ограничений на значения параметров события и переменных верифицируемой модели и что совместное постусловие событий в каждой цепочке влечет постусловие соответствующего этой цепочке события верифицируемой модели, затем проверяют выполнение инвариантов более простой автоматной модели во всех ее состояниях, затем проверяют выполнение инвариантов верифицируемой формальной автоматной модели в ее начальных состояниях, затем проверяют выполнение во всех состояниях инвариантов верифицируемой формальной автоматной модели, не входящих в простую модель, и по результатам проверок делают заключение о корректности верифицируемой модели.

2. Способ верификации формальной автоматной модели поведения программной системы по п. 1, отличающийся тем, что выбирают более простую автоматную модель из уже существующих, для которой переменные являются подмножеством переменных верифицируемой модели, инварианты являются подмножеством инвариантов верифицируемой модели, зависящих только от переменных более простой модели, и каждое событие верифицируемой формальной автоматной модели либо определяет изменение только не входящих в более простую автоматную модель переменных и называется вспомогательным, либо эквивалентно выполнению цепочки из вспомогательных событий и событий более простой автоматной модели, причем выбор такой цепочки однозначно определяется значениями параметров события и переменных верифицируемой формальной автоматной модели.