1

Размещено на http://www.allbest.ru/

УДК 519.713.1

Институт кибернетики им. В.М.Глушкова НАН Украины

Доказательное проектирование алгоритмов функционирования реактивных систем

Чеботарев А.Н., Головинский А.Л.

ancheb@gmail.com, golovinsky.andriy@gmail.com

Аннотация

проектирование реактивный кибернетика логический

Описывается подход к доказательному проектированию реактивных алгоритмов, развиваемый в Институте кибернетики имени В.М. Глушкова НАН Украины, рассматриваются основные проблемы, возникающие при проектировании реактивных алгоритмов, специфицированных в логическом языке L, и методы их решения.

Abstract

An approach to provably-correct design of reactive algorithms is described, that has been developed at the Glushkov Institute of Cybernetics of the Ukrainian Academy of Sciences. The basic problems arising in the design of reactive algorithms specified in the logical language L, and methods to solve them are considered.

Анотація

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

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

В методах корректного проектирования реактивных алгоритмов, используемых на начальных этапах их разработки, можно выделить два основных подхода:

а) формальная верификация неформально полученного процедурного представления алгоритма,

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

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

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

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

В настоящей статье описывается подход к доказательному проектированию реактивных алгоритмов, развиваемый в Институте кибернетики имени В.М. Глушкова НАН Украины, рассматриваются основные проблемы, возникающие при проектировании реактивных алгоритмов, специфицированных в языке L, и методы их решения.

Язык спецификации

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

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

Идея использования логического языка для спецификации конечных автоматов восходит к работам Черча [1], Бюхи [2] и Б.А. Трахтенброта [3, 4]. В этих работах построен ряд языков, основанных на логике одноместных предикатов от натурального аргумента, и приведены соответствующие алгоритмы синтеза автоматов. Однако полученные в то время результаты не стимулировали применения логических методов для спецификации и проектирования программ или схем, поскольку носили сугубо теоретический характер. В настоящее время существует большое количество языков для спецификации реактивных алгоритмов. К ним относятся языки, основанные на различных темпоральных логиках, наибольшее распространение из которых получили LTL [5], CTL [6], CTL* [7], а также языки, основанные на операторах наименьшей и наибольшей неподвижной точки [8]. Эти языки, как правило, используются в системах верификаии, однако сложность решения для них задач синтеза такова, что вряд ли можно надеяться на применение их для решения практических задач. Существенного увеличения эффективности алгоритмов синтеза можно добиться путем разумного ограничения выразительных возможностей языка спецификации. При этом приходится искать компромисс между выразительными возможностями языка и сложностью алгоритмов проектирования. Для разрешения этого противоречия предлагается использовать два уровня языка: язык исходной спецификации L* [9], обладающий достаточными для практических нужд выразительными возможностями и обеспечивающий удобство записи исходных требований к алгоритму, и внутренний язык L [10], обладающий сравнительно ограниченными выразительными возможностями, но эффективно обрабатываемый процедурами синтеза. Отметим, что название «внутренний язык» довольно условное, поскольку во многих случаях он может выступать в качестве языка исходной спецификации. Оба языка построены на основе соответствующих фрагментов логики предикатов первого порядка с одноместными предикатами, определенными на множестве моментов дискретного времени, в качестве которого выступает множество Z целых чисел. При этом имеется возможность спецификацию в языке L* преобразовать в спецификацию в языке L.

Спецификация в языке L имеет вид tF(t), где F(t) -- формула, построенная с помощью логических связок из атомов вида p(t + k). Здесь p -- предикатный символ, t -- переменная, принимающая значения из множества Z, а k -- целочисленная константа (сдвиг во времени), называемая рангом соответствующего атома. Язык L* отличается от языка L тем, что при построении F(t) используется еще конструкция: $ti(ti t + k1)&F1(ti)&tj((ti + k2 tj t + k3) F2(tj)), где k1, k2, k3 Z, F2(tj) -- формула языка L, а F1(ti) -- формула языка L*.

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

Пусть -- конечный алфавит, Z -- множество целых чисел и N⁺ = {z Z z 0}. Отображения u: Z и l: N⁺  называются соответственно двусторонним сверхсловом (обозначается …u(2)u(1)u(0)u(1)u(2)…) и сверхсловом (обозначается l(1)l(2)… ) в алфавите . Для двустороннего сверхслова u и n Z определим n-суффикс u(n+1, ) как сверхслово u(n+1)u(n+2)….

Конечный неинициальный X-Y-автомат Мили A -- это четверка A = <X, Y, Q, >, где X, Y, Q -- конечные множества соответственно входных символов, выходных символов и состояний, а : QXY 2^Q -- функция переходов автомата.

X-Y-автомат Мили называется квазидетерминированным, если для любых q Q, x X, y Y |(q, x, y)| 1. Квазидетерминированные X-Y-автоматы удобно рассматривать как детерминированные частичные автоматы без выхода, с входным алфавитом = XY. Такой автомат A = <, Q, >, где : Q Q -- частичная функция, будем называть -автоматом.

-автомат A = , Q, называется циклическим, если для каждого q Q существуют такие , и q₁, q₂ Q, что q₁ (q, ₁) и q (q₂, ₂).

Циклический автомат может быть однозначно охарактеризован в терминах допустимых сверхслов.

Сверхслово l = ₁,₂, … в алфавите допустимо в состоянии q автомата A, если существует такое сверхслово состояний q₀q₁q₂…, где q₀ = q, что для любого i = 0, 1, 2, …? q_i+1 = (q_i, _i+1). Сверхслово l допустимо для автомата A, если оно допустимо в каком-либо из его состояний.

Перейдем теперь к описанию сверхсловарной семантики языка L. Каждой замкнутой формуле F ставится в соответствие множество моделей для этой формулы, т.е. множество таких интерпретаций, на которых F истинна. Пусть = {p₁, …, p_m} -- множество всех одноместных предикатных символов, встречающихся в формуле F. Интерпретация формулы F -- это упорядоченный набор определенных на Z одноместных предикатов _{1 m}, соответствующих предикатным символам из . Пусть -- множество всех двоичных векторов длины m, тогда интерпретацию I = <_{1 m}>, можно представить в виде двустороннего сверхслова в алфавите , а множество всех моделей для F -- в виде множества M_F двусторонних сверхслов в этом алфавите. Будем полагать, что формула F = tF(t) языка L задает множество всех 0-суффиксов двусторонних сверхслов из M_F.

Теорема 1 [11]. Для всякой непротиворечивой формулы F вида tF(t) существует в общем случае частичный неинициальный циклический автомат A, для которого множество всех допустимых сверхслов совпадает с множеством сверхслов, задаваемых формулой F.

Это определяет автоматную семантику языка L.

Проверка непротиворечивости

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

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

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

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

Пусть c₁ и c₂ -- нормализованные вправо дизъюнкты, p(t) -- атом нулевого ранга и c₁ = c₁ p(t), а c₂ = c₂ p(t). Дизъюнкт c = c₁ c₂ называется R-резольвентой дизъюнктов c₁ и c₂ по атому p(t).

Операцию получения R-резольвенты двух дизъюнктов будем называть R-резольвированием.

R-выводом дизъюнкта c из множества дизъюнктов C называется такая конечная последовательность дизъюнктов с₁, ..., c_k, что c_k = c и каждый дизъюнкт c_i (i = 1, ..., k) либо принадлежит C, либо является R-резольвентой двух предшествующих дизъюнктов, либо есть результат нормализации вправо дизъюнкта c_i-1.

Справедливо следующее утверждение. Множество С нормализованных вправо дизъюнктов противоречиво тогда и только тогда, когда существует R-вывод пустого дизъюнкта из C.

Процесс проверки непротиворечивости множества дизъюнктов С можно представить в виде поочередного выполнения следующих двух операций:

а) построение замыкания С относительно резольвирования по атомам нулевого ранга,

б) нормализация вправо всех ненормализованных дизъюнктов.

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

Дизъюнкт c₁(t) поглощает дизъюнкт c₂(t), если существует такое k Z, что все литеры из c₁(t+ k) содержатся среди литер дизъюнкта c₂(t). Удаление из множества дизъюнктов, представляющих формулу tF(t), дизъюнктов, поглощаемых другими дизъюнктами этого множества, приводит к множеству дизъюнктов, задающих формулу, эквивалентную (т.е. имеющую то же множество моделей в рассматриваемом классе интерпретаций) формуле tF(t).

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

Теорема 2 [12]. Формула tF(t), заданная множеством С нормализованных вправо дизъюнктов, невыполнима тогда и только тогда, когда в процессе пополнения С будет получен пустой дизъюнкт.

Эффективность рассмотренного метода обусловлена сокращением множества порождаемых дизъюнктов за счет ограничения вида литер, по которым допускается резольвирование, литерами нулевого ранга. При этом отпадает необходимость выполнения унификации, что также повышает эффективность метода. В [13, 14] описаны усовершенствования рассмотренного метода, связанные с разбиением множества дизъюнктов на несколько классов и запрещением резольвирования дизъюнктов, принадлежащих различным классам, что существенно сокращает количество дизъюнктов, порождаемых в процессе пополнения.

Синтез

Методы синтеза управляющей части алгоритма основаны на теореме о спецификации [9], устанавливающей связь между структурой некоторого представления формулы в языке спецификации и структурой соответствующего автомата, определенной в терминах множества состояний и функций переходов и выходов. Это приводит к понятию нормальной формы формулы F(t) языка L.

Пусть F(t) = F_i(t1)&f_i(t), где F_i(t1) -- формула, максимальный ранг атомов в которой не превышает 1, а f_i(t) -- формула, построенная из атомов ранга 0. Представление F(t) в таком виде будем называть дизъюнктивным представлением, а конъюнкцию вида F_i(t1)&f_i(t) -- компонентой такого представления с левой частью F_i(t1) и правой частью f_i(t). Дизъюнктивное представление удовлетворяет условию ортогональности, если для i j (i, j {1, …, n}) F_i(t1)&F_j(t1) 0. Дизъюнктивное представление формулы F(t), удовлетворяющее условию ортогональности, называется нормальной формой, если для любых i, j = 1, …, n конъюнкция F_i(t1)&f_i(t)&F_j(t) либо тождественно равна нулю, либо равна F_i(t1)&f_ij(t), где f_ij(t) -- не равная тождественно нулю формула, построенная из атомов нулевого ранга.

Пусть = {p₁, …, p_q} -- множество всех предикатных символов, встречающихся в F(t), а -- множество всех двоичных векторов длины q. Символу () соответствует элементарная конъюнкция (t) вида (t)& … &(t), где (t) {p_j(t), p_j(t)}. Спецификации F = tF(t), в которой F(t) представлена в нормальной форме, соответствует -автомат A(F) с входным алфавитом (), состояниями q₁, …, q_n и функцией переходов , определяемой следующим образом. Для и q_i, q_j {q₁, …, q_n} (q_i, ) = q_j тогда и только тогда, когда F_i(t1)& f_i(t)&(t)&F_j(t) = F_i(t1)&(t). Из теоремы о спецификации следует, что автомат A(F), удовлетворяет спецификации F.

Построение автомата A(F) состоит из двух основных этапов: 1) построения дизъюнктивного представления формулы F(t), удовлетворяющего условию ортогональности, и 2) построения нормальной формы формулы F(t).

На первом этапе требуемое представление получается путем последовательного применения к парам компонент дизъюнктивного представления соотношения:

F_i(t1)&f_i(t) Ъ --F_j(t1)&f_j(t) F_i(t1)&ШF_j(t1)&f_i(t) Ъ-- ШF_i(t1)&F_j(t₁)&f_j(t) Ъ Ъ--F_i(t1)&F_j(t1)&(f_i(t)Ъ--f_j(t)).

На втором этапе для получения нормальной формы формулы F(t) осуществляется расщепление компонент ее дизъюнктивного представления путем умножения их на F_i(t). Эквивалентность такого преобразования формулы F(t) показана в [15]. Результат расщепления компоненты определяется дизъюнктивным представлением полученного произведения, удовлетворяющим условию ортогональности. Расщепления компоненты F_i(t1)&f_i(t) не происходит, если в таком дизъюнктивном представлении произведения все компоненты имеют левую часть F_i(t1). Процесс продолжается до тех пор, пока на очередном шаге ни одна из компонент не будет расщеплена. Описанный метод синтеза реализован в виде команды “dual” в системе синтеза и верификации дискретных устройств MVSIS, разработанной в Калифорнийском университете, в Беркли, США (http://www.ece.pdx.edu/~alanmi/mvsis/exe).

В [16] предложен метод синтеза инициального автомата, не требующий какого-либо специального представления формулы F(t). Он может применяться как к д.н.ф., так и к любому другому представлению формулы. Результат синтеза получается путем индуктивного построения автомата в соответствии со структурой формулы F(t), т.е. элементарные акты синтеза соответствуют основным логическим операциям, применяемым при построении формулы F(t). Сходный метод синтеза используется в системе MONA [17], реализующей разрешающую процедуру для слабой теории второго порядка функции следования (WS1S). Однако там язык спецификации интерпретируется на множестве конечных слов и в качестве автомата рассматривается модель распознавателя (автомат Бюхи).

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

Синтез открытых систем

Для возможности корректной реализации реактивного алгоритма (представляющего собой открытую систему) одной внутренней непротиворечивости спецификации недостаточно. Непротиворечивость спецификации гарантирует только то, что существует совместное поведение внешней среды и синтезируемого алгоритма, которое удовлетворяет спецификации. Поскольку поведение среды не может быть регламентировано, необходимо, чтобы на любое допустимое ее поведение алгоритм реагировал таким образом, чтобы их совместное поведение удовлетворяло спецификации. Обычно соответствующая проблема синтеза формулируется как нахождение выигрышной стратегии в бесконечной игре между средой и системой [18]. Эта стратегия представляется в виде бесконечного размеченного дерева. Для описания всех допустимых (т.е. удовлетворяющих спецификации) стратегий строится автомат Рабина над бесконечными деревьями [19], такой, что множество всех бесконечных деревьев, распознаваемых автоматом, соответствует всем стратегиям, реализующим исходную спецификацию. Таким образом, проверка реализуемости спецификации сводится к проверке непустоты языка, представляемого автоматом Рабина. Алгоритм проверки непустоты автомата Рабина позволяет получить конечное представление бесконечного дерева, распознаваемого автоматом, которое затем преобразуется в синтезируемый алгоритм. В целом такая процедура синтеза требует времени выражающегося в виде двойной экспоненты от размера спецификации. Приведенная оценка вряд ли может быть улучшена, поскольку, как показано в [20], проблема синтеза в рассмотренной постановке полна в классе 2EXPTIME. В [21] получено решение проблемы синтеза с существенно лучшей оценкой сложности за счет ограничения языка спецификации подмножеством GR(1) темпоральной логики LTL.

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

При формализации проблемы согласованности рассматриваются частичные недетерминированные X-Y-автоматы Мура вида A = <X, Y, Q, , >, где : Q X 2^Q и : Q Y -- соответственно функции переходов и выходов. Если |X| = 1, то автомат A называется автономным Y-автоматом, который определяется четверкой <Y, Q, , >. Функция переходов такого автомата имеет вид _A: Q 2^Q.

Пусть A = <X, Y, Q_A, _A, _A> и B = <Y, X, Q_B, _B, _B> -- частичные недетерминированные соответственно X-Y- и Y-X-автоматы Мура.

Симметричная циклическая композиция автоматов А и В представляет собой автономный недетерминированный Z-автомат Мура С = <Z, Q_C, _C, _C>, где Z = XY YX, Q_C = Q_AQ_B Q_BQ_A, а функция переходов _C и функция выходов _C определяются следующим образом. Для всех q Q_A и s Q_B

_C(q, s) = {(s, q₁) | q_{1 A}(q, _B(s))},

_C(s, q) = {(q, s₁) | s_{1 B}(s, _A(q))},

_C(q, s) = (_A(q), _B(s)), _C(s, q) = (_B(s), _A(q)).

Два циклических частичных детерминированных X-Y- и Y-X-автомата Мура называются согласованными, если их симметричная циклическая композиция имеет циклический подавтомат.

Понятие согласованности недетерминированных автоматов связано с понятием циклической детерминизации недетерминированного автомата [23].

_{Частичный недетерминированный циклический X-Y-автомат Мура А согласован с частичным недетерминированным циклическим Y-X-автоматом Мура В, если существует циклическая детерминизация автомата A, согласованная с каждой циклической детерминизацией автомата B.}

Такое определение неконструктивно, поскольку количество детерминизаций автомата бесконечно, поэтому в [24] оно переформулируется в терминах конструктивного свойства параллельной циклической композиции. Решение проблемы рассматривается для случая, когда оба взаимодействующих автомата специфицированы множествами дизъюнктов. В основе соответствующего алгоритма лежат две процедуры: удаление из управляющей компоненты проектируемого алгоритма состояний, задаваемых формулой языка L, и проверка непротиворечивости (пополнение) множества дизъюнктов. Первая из этих процедур, так же как и вторая, реализована в виде преобразования множества дизъюнктов. Существенной особенностью метода, обеспечивающей его эффективность, является то, что не требуется рассматривать произведение взаимодействующих автоматов, т.е. объединение соответствующих множеств дизъюнктов.

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

Верификация

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

Верификация формально синтезированных алгоритмов имеет свои особенности: 1) не требуется построения автоматной модели верифицируемой системы (она получается в результате синтеза) и 2) не нужно верифицировать свойства алгоритма, определяемые исходной спецификацией. В качестве языка для спецификации верифицируемых свойств алгоритма используется усовершенствованный вариант темпоральной логики с линейным временем, а верификация осуществляется методом проверки выполнимости формулы на модели (model checking) [25].

Заключение

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

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

Литература

1. Church A. Applications of recursive arithmetic to the problem of circuit synthesis // Summaries of the summer Inst. for Symbolic Logic. -- New York: Cornell Univ., 1957. -- P. 3-50.

2. Bьchi J.R. Weak second-order arithmetic and finite automata // Zeitschr. Math. Logik und Grundl. der Math. -- 1960. -- Vol. 6, N1. -- P. 66-92.

3. Трахтенброт Б.А. Синтез логических сетей, операторы которых описаны средствами исчисления одноместных предикатов // ДАН СССР. -- 1958. -- Т. 118, №4. -- С. 646-649.

4. Трахтенброт Б.А. Конечные автоматы и логика одноместных предикатов // Сиб. мат. журн. -- 1962. -- Т. 3, №1. -- С. 103-131.

5. Pnueli A. The temporal logic of programs // Proc. of the 18^th Symp. on foundations of computer sci. -- New York: IEEE Computer Society Press, 1977. -- P. 46-57.

6. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic // LNCS. -- 1981. -- Vol. 131. -- P. 52-71.

7. Emerson E.A., Halpern J. Y. “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic // J. ACM. -- 1986. -- 33, -- № 1. -- P. 157 - 178.

8. Stomp F.A., de Roever W.P., Gerth R.T. The -calculus as an assertion language for fairness arguments // Information and computation. -- 1989. -- Vol. 82. -- P. 278-322.

9. Чеботарев А.Н. Расширение логического языка спецификации автоматов и проблема синтеза // Кибернетика и системный анализ. -- 1996, №6, 11-27.

10. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. I // Кибернетика и системный анализ. -- 1993, №3, 31-42.

11. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. II // Кибернетика и системный анализ. -- 1993, №4, 3-14.

12. Чеботарев А.Н. Проверка непротиворечивости простых спецификаций автоматных систем // Кибернетика и системный анализ. -- 1994, №3, 3-11.

13. Чеботарев А.Н. Метод раздельного резольвирования для проверки выполнимости формул языка L // Кибернетика и системный анализ. -- 1998, №6, 13-20.

14. Крывый С.Л., Чеботарев А.Н. Усовершенствованный метод проверки выполнимости множества дизъюнктов в языке L. Таврический вестник информатики и математики, 2006, №1. 7 - 13

15. Чеботарев А.Н. Синтез процедурного представления автомата, специфицированного в логическом языке L*. I, II // Кибернетика и системный анализ. - 1997, N4, 60-74, N6, 115-127.

16. Капитонова Ю.В., Чеботарев А.Н. Индуктивный синтез автомата по спецификации в логическом языке L // Кибернетика и системный анализ. -- 2000, №6, 3-13.

17. Mona: monadic second-order logic in practice / J.G. Henriksen, J. Jensen, M. Jorgensen et al. // LNCS. -- 1996. -- Vol. 1019. -- P. 89-110.

18. Abadi M., Lamport L. Composing specifications // ACM Trans/ on Programming Languages and Systems. -- 1993. --Vol. 15. -- P. 73-132.

19. Thomas W. Automata on infinite objects // Handbook of theoretical computer science, ed. J.van Leeuwen. -- Amsterdam: Elsevier Sci. Publ., 1990. -- P. 134-191.

20. Pnueli A., Rosner R. On the synthesis of a reactive module // Proc. 16^th Annual ACM Symp. on Principles of Programming Languages. -- ACM, 1989. -- P. 179-190.

21. Piterman N., Pnueli A. and Sa'ar Y. Synthesis of reactive(1) designs // Proc. of Conf. on Verification, Model Checking and Abstract Interpretation. -- 2006, . -- P. 364-380.

22. Чеботарев А.Н. Взаимодействие автоматов // Кибернетика. -- 1991, №6, 17-29.

23. Чеботарев А.Н. Детерминизация логических спецификаций автомаов // Кибернетика и системный анализ. -- 1995, №1, 3-12.

24. Мороховец М.К., Чеботарев А.Н. Резолюционный подход к проверке согласованности взаимодействующих автоматов. // Кибернетика и системный анализ. -- 1994, №6 36-50.

25. Чеботарев А.Н. Теоретико-автоматный подход к верификации реактивных систем. // Кибернетика и системный анализ. -- 2001, №6, 37-49.

Размещено на Allbest.ru