Программирование, 2020, № 4, стр. 14-26

1. ВВЕДЕНИЕ

Растущая сложность систем управления, используемых в нашей повседневной жизни, требует переоценки инструментов проектирования и разработки. Такая переоценка особенно важна для критических с точки зрения безопасности систем, где неправильное поведение и/или отсутствие надежности может привести к неприемлемой потере средств или даже человеческой жизни. Такие системы широко распространены в промышленности, особенно на химических и металлургических заводах. Поскольку поведение сложных систем управления определяется программным обеспечением, исследование управляющего программного обеспечения представляет большой интерес. Корректное поведение в различных условиях окружающей среды должно быть гарантировано. При отказе оборудования, например, поломках механических частей объекта управления или исполнительных устройств, система должна автоматически сформировать управляющие воздействия, которые предотвращают опасные последствия таких отказов. Общепринятое название этого свойства системы управления – отказоустойчивость (fault tolerant behavior) [1].

Из-за специфики предметной области системы управления обычно основаны на промышленных контроллерах, также известных как программируемые логические контроллеры (ПЛК), и специализированные языки используются для проектирования управляющего программного обеспечения для таких систем. Наиболее распространенными в области программирования ПЛК являются языки стандарта IEC 61131-3 [2]. Однако, поскольку сложность управляющего программного обеспечения возрастает, а качество становится более приоритетным, 35-летняя технология, основанная на подходе IEC 61131-3, не всегда способна удовлетворить современные требования [3]. Поэтому исследователи предпринимают попытки либо модифицировать модель разработки IEC 61131-3, например, обогатить модель объектно-ориентированными концепциями [4], либо вообще предложить взамен IEC 61131-3 альтернативные понятийно-языковые средства, например, [5–8].

Для устранения ограничений и проблем при разработке современного комплексного управляющего программного обеспечения в [9] была предложена парадигма процесс-ориентированного программирования. Эта парадигма представляет управляющее программное обеспечение в виде набора взаимодействующих процессов, где процессы – это конечные автоматы, дополненные неактивными состояниями и специальными функциями управления процессами и обработки временных интервалов. По сравнению с известными модификациями конечных автоматов, например, последовательными взаимодействующими процессами [10], диаграммами состояний Харела [11], автоматами ввода/вывода [12], Esterel [13], гибридными автоматами [14], исчислением взаимодействующих систем [15] и их временными расширениями [16, 17], этот метод обеспечивает средства для спецификации параллелизма и при этом сохраняет линейность потока управления на уровне процесса. Таким образом, он обеспечивает концептуальную основу для разработки процессно-ориентированных языков, предназначенных для создания программного обеспечения для ПЛК. Процесс-ориентированный подход был реализован в таких предметно-ориентированных языках как SPARM [18], Reflex [19] и IndustrialC [20]. Эти языки являются C-подобными и, поэтому, просты в изучении. Трансляторы для них порождают C-код, который обеспечивает кросс-платформенную переносимость. Благодаря прямой поддержке конечных автоматов и операций с плавающей запятой, эти языки позволяют достаточно просто создавать программное обеспечение для ПЛК.

Язык SPARM является предшественником языка Reflex и в настоящее время не используется. IndustrialC нацелен на использование периферийных устройств микроконтроллера (регистров, таймеров, ШИМ и т.д.) и расширяет Reflex средствами обработки прерываний. Программа на языке Reflex специфицируется как набор взаимодействующих параллельных процессов. Reflex включает специализированные инструкции для управления процессами и обработки временных интервалов. Он также предоставляет инструкции для связывания программных переменных с физическими сигналами ввода/вывода. Процедуры чтения/записи данных через регистры и их сопоставление с переменными порождаются транслятором автоматически.

Reflex предполагает цикл управления с фиксированным временем исполнения и строгую инкапсуляцию зависимых от платформы подпрограмм ввода-вывода в библиотеку, что является широко применяемым методом в системах на основе IEC 6113-3. Для обеспечения простоты поддержки и межплатформенной переносимости генерация исполняемого кода осуществляется в два этапа: транслятор Reflex генерирует C-код, а затем C-компилятор создает исполняемый код для целевой платформы. Reflex – простой язык с точки зрения операторов и типов данных. Он не имеет указателей, массивов и циклов. Несмотря на простоту, этот язык был успешно применен в нескольких индустриальных системах управления, например, в программном обеспечении для управления печью установкой для выращивания монокристаллического кремния [21]. Семантическая простота языка вместе с практической применимостью делает Reflex привлекательным для теоретических исследований.

В настоящее время проект Reflex сфокусирован на средствах проектирования и разработки критических с точки зрения безопасности систем. Благодаря своей системной независимости Reflex легко интегрируется со сторонними средствами, например, с LabVIEW [22]. Это позволяет разрабатывать программное обеспечение, сочетающее управляемое событиями поведение с расширенным графическим интерфейсом пользователя, удаленными датчиками и исполнительными устройствами, устройствами с поддержкой LabVIEW и т.д. Используя гибкость LabVIEW, был разработан набор тренажеров для учебных целей [23]. Основанные на LabVIEW симуляторы включают в себя 2D-анимацию, инструменты для отладки и языковую поддержку для обучения разработке управляющего программного обеспечения. Одним из результатов, полученных в этом направлении, является набор инструментов динамической верификации на основе LabVIEW для Reflex-программ. Динамическая верификация рассматривает программное обеспечение как черный ящик и проверяет его соответствие требованиям, наблюдая за поведением программного обеспечения во время выполнения на наборе тестовых случаев. Хотя такая процедура может помочь обнаружить наличие ошибок в программном обеспечении, она не может гарантировать их отсутствие [24].

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

В этой статье мы предлагаем метод дедуктивной верификации Reflex-программ. Оригинальная двухшаговая схема метода позволяет нам свести проверку временных свойств Reflex-программ к дедуктивной верификации С-подобной программы, которая явно моделирует время и историю выполнения Reflex-программы.

Работа имеет следующую структуру. В разделе 2, мы формулируем подход к спецификации временных свойств Reflex-программ и пример Reflex-программы, управляющей сушилкой для рук, а также ее временные свойства. В разделе 3 на примере программы управления сушилкой для рук описывается алгоритм трансляции аннотированных Reflex-программ в язык VOL[Reflex] (Verification-Oriented Language) – ограниченное подмножество аннотированных императивных программ на языке C, расширенное логическим типом bool и супертипом value, объединяющем значения, которые могут возвращать функции и операции языка Reflex, а также оператором havoc $x$, присваивающем произвольное значение переменной $x$. В разделе 4 представлена формальная трансляционная семантика языка Reflex в язык VOL[Reflex] (далее VOL), описывающая правила трансляции Reflex-инструкций в VOL-инструкции. Трансляция аннотированной Reflex-программы в VOL-программу – первый шаг нашего метода дедуктивной верификации. Второй шаг – дедуктивная верификация VOL-программы, состоящая в порождении условий корректности для нее и их доказательстве, – определяется в разделе 5. Он включает алгоритм порождения условий корректности и примеры условий корректности для VOL-программы – результата трансляции программы управления сушилкой для рук. В заключительном разделе 6 мы обсуждаем особенности нашего метода и направления будущих исследований.

2. СПЕЦИФИКАЦИЯ ВРЕМЕННЫХ СВОЙСТВ REFLEX-ПРОГРАММ

Наш метод верификации сводит верификацию Reflex-программ к верификации VOL-программ. Reflex-программа вместе с ее проверяемыми временными свойствами транслируется в эквивалентную VOL-программу с соответствующим набором проверяемых свойств. В этом разделе мы определим подход к спецификации для свойств Reflex-программ. Этот подход иилюстрируется на примере Reflex-программы, управляющей сушилкой для рук.

Мы специфицируем свойства Reflex-программ, используя два языка: язык аннотаций и язык аннотаторов. Язык аннотаций – это язык логических формул – аннотаций, описывающих свойства программы. Язык аннотаторов – это язык разметки, сопоставляющий аннотации конструкциям программы. Элементы этого языка называются аннотаторами. Программа, расширенная аннотаторами, называется аннотированной программой.

Аннотации Reflex-программ являются формулами многосортной логики первого порядка, представленными в синтаксисе интерфейса Z3py [25] к SMT-решателю Z3 [26], который используется для доказательства условий корректности, порождаемых для VOL-программ – результатов трансляции Reflex-программ.

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

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

Время в аннотациях моделируется глобальным таймером и локальными таймерами процессов. Таймеры задаются переменными типа int. Эти переменные не могут быть переменными Reflex-программы. Глобальный таймер timer подсчитывает число тактов работы Reflex-программы. Каждый программный процесс ${{p}_{i}}$ имеет свой локальный таймер ${{p}_{i}}$_{_timer}, который также как и глобальный таймер считает время в количестве тактов работы программы.

Каждая программная переменная x интерпретируется в аннотациях как массив, в котором индекс i означает i-й цикл выполнения программы, а элемент x[i] хранит значение переменной x на этом цикле. Таким образом, в контексте аннотации, x хранит историю своих изменений.

Аннотации также используют следующие переменные:

• val – для доступа к значению, возвращаемую функцией или операцией в Reflex-программе;

• val_1, …, val_n – для хранения значений аргументов функций и операций, вычисляемых в Reflex-программе (n – максимальная местность функций и операций, используемых в программе);

• p_{i_state} – для доступа к текущему состоянию программного процесса p_i.

Обозначим множество аннотаций F, так что $f \in F$ является аннотацией, специфицирующей некоторое свойство Reflex-программы.

Язык аннотаторов для Reflex-программ включает четыре вида аннотаторов. Инвариантный аннотатор INV f; специфицирует, что свойство f должно выполняться перед каждым программным циклом. Аннотатор начального условия ICON f; специфицирует, что свойство f должно выполняться перед первым программным циклом. Аннотатор внешнего условия ECON f; накладывает ограничения на внешние модификации переменных: свойство f должно выполняться после каждой внешней модификации. Аннотатор функций REQUIRES ${{P}_{f}}$; ENSURES ${{Q}_{f}}$; должен размещаться непосредственно после прототипа функции t f (${{t}_{1}}$ x₁, ..., ${{t}_{n}}$ x_n). Прототипы функций используются чтобы вызывать функции, написанные на других языках программирования, в Reflex-программах. Этот аннотатор специфицирует предусловие ${{P}_{f}}$ и постусловие ${{Q}_{f}}$ функции  f. Формулы ${{P}_{f}}$ и ${{Q}_{f}}$ зависят от ${{x}_{1}}, \ldots ,{{x}_{n}}$. Постусловие ${{Q}_{f}}$ также зависит от val, которая хранит значение, возвращаемое  f.

Проиллюстрируем наш подход к спецификации временных свойств на примере программы управления сушилкой для рук (рис. 1, Листинг 1).

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

Сформулируем несколько временных свойств для этой программы. Первое свойство заключается в том, что сушилка должна включиться за время, приемлемое с точки зрения пользователя (не позднее 100 миллисекунд), когда под ней появляются руки. Второе свойство постулирует, что сушилка никогда не включается произвольно. Эти свойства задаются ниже формулами ${{r}_{1}}$ и ${{r}_{2}}$.

PROGR HandDryerController {

/* =========================== */

/* == ANNOTATIONS : */

/* INV inv; */

/* ICON True ; */

/* ECON True ; */

/* == END OF ANNOTATIONS */

TACT 100;

CONST ON TRUE ;

CONST OFF FALSE ;

/* ============================= */

/* I/O ports specification */

/* direction , name , address , */

/* offset , size of the port */

/* ============================= */

INPUT SENSOR_PORT 0 0 8;

OUTPUT ACTUATOR_PORT 1 0 8;

/* ============================= */

/* processes definition */

/* ============================= */

PROC Ctrl {

 /* ===== VARIABLES ============= */

 BOOL hands = { SENSOR_PORT [1]} FOR ALL;

 BOOL dryer = { ACTUATOR_PORT [1]} FOR ALL;

 /* ===== STATES ================ */

 STATE Waiting {

   IF ( hands == ON) {

    dryer = ON;

    SET NEXT ;

   } ELSE dryer = OFF;

 }

 STATE Drying {

   IF ( hands == ON) RESET TIMEOUT ;

   TIMEOUT 10 SET STATE Waiting ;

 }

} /* \ PROC */

} /* \ PROGRAM */

Листинг 1: Reflex-программа управления сушилкой для рук

В Reflex-программах инструкция PROGR специфицирует имя и тело программы. Аннотаторы добавляются в начало тела программы как специальный вид комментариев. В нашем случае аннотаторами являются INV inv;, ICON True; и ECON True; (аннотация inv определена ниже). Инструкция TACT специфицирует число миллисекунд, соответствующее одному программному циклу. Инструкция CONST используется для объявления программных констант. Инструкции INPUT и OUTPUT описывают входные и выходные порты, соответственно. Программные переменные определяются через объявления переменных. Например, объявление переменной BOOL hands = SENSOR_PORT[1] FOR ALL связывает логическую переменную hands с первым битом порта SENSOR_PORT и указывает, что все процессы могут использовать эту переменную. Инструкция PROC используется для описания процессов программы. В нашем примере программа имеет один процесс Ctrl (контроллер), который управляет сушилкой для рук, то есть вентилятором и обогревателем. Инструкция STATE объявляет возможные состояния процесса. Процесс Ctrl может находиться в двух состояниях WAITING и DRYING. Действия, выполняемые процессом в состоянии, описываются в теле этого состояния с помощью операторов и операций.

В дополнении к С-подобным операторам и операциям, язык Reflex включает ряд специализированных операторов и операций для работы с процессами. Оператор RESET TIMEOUT; сбрасывает локальный таймер текущего процесса. Оператор TIMEOUT $x$ stm; запускает выполнение оператора stm, когда локальный таймер текущего процесса достигает значения x. Оператор SET NEXT; переключает текущий процесс в следующее состояние (в порядке, в котором состояния объявляются в теле процесса), а оператор SET STATE s; переключает процесс в состояние s. Эти два оператора также обнуляют локальный таймер процесса.

Программа управления сушилкой не накладывает ограничения на начальное и внешнее условия. Они определяются как True. Заметим, что если бы язык проекций не включал тип bool как в [27] и константы ON и OFF определялись бы как 1 и 0, то эти условия имели бы вид:

$And(Or($dryer[0]==0, dryer[0]==1),

          Or(hands[0]==0, hands[0]==1)

и

Or(hands[timer]==0, hands[timer]==1),

специфицируя, что переменные dryer и hands могут принимать только значения 0 и 1. Включение типа bool позволяет упростить аннотации и, соответственно, порождаемые условия корректности.

Инвариант inv вида $And({{r}_{1}},{{r}_{2}},ap)$ включает свойства ${{r}_{1}}$ и ${{r}_{2}}$, которые специфицируют желаемое поведение программы и конъюнкцию ap вспомогательных свойств, необходимых для их верификации. Эти вспомогательные свойства формулируются следующим образом: 1) значения программных констант равны их преодопределенным значениям, 2) глобальный таймер и все локальные таймеры неотрицательны, 3) текущие значения переменных hands и dryer совпадают с их предыдущими значениями (это свойство обеспечивает переход на новый такт выполнения программы), 4) сушилка может находиться только в двух состояниях WAITING и DRYING, и 5) сушилка в состоянии DRYING всегда включена. Мы опускаем формальную спецификацию для ap, так как она довольно громоздка.

Свойство ${{r}_{1}}$ вида

 $ForAll(i,$

     $Implies($

        $And(0 < = i,i < timer),$

        $Implies($

             $And($

                $Implies(i > 0,$ hands[i – 1]==OFF),

      hands[i]==ON),

             dryer[i]==ON)))

специфицирует, что сушилка включается (dryer[i]==ON) не позднее, чем через 100 миллисекунд (один такт) после появления рук.

Свойство ${{r}_{2}}$ вида

 $ForAll(i,$

    $Implies($

       $And(0 < = i,i < timer - 1),$

       $Implies($

          $And($dryer[i]==OFF,

          hands[i + 1]==OFF),

          dryer[i + 1]==OFF)))

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

В следующем разделе мы представим на примере программы управления сушилкой для рук алгоритм трансляции аннотированной программы Reflex в VOL-программу, для которой порождаются условия корректности.

3. ТРАНСЛЯЦИЯ АННОТИРОВАННОЙ REFLEX-ПРОГРАММЫ В VOL-ПРОГРАММУ

Reflex-программы и VOL-программы используют один и тот же язык аннотаций. Язык аннотирования для VOL-программ включает аннотатор функций и три дополнительных аннотатора. Аннотатор ASSUME  f; специфицирует, что  f считается истинной в точке размещения этого аннотатора в программе. Аннотатор ASSERT  f; утверждает, что f должна быть истинной в точке размещения этого аннотатора в программе. Инвариантный аннотатор INV l f; – специальный вариант именованного ASSERT-аннотатора с именем l, который обрабатывается специальным образом нашим алгоритмом порождения условий корректности.

VOL-программа – результат трансляции Reflex-программы управления сушилкой для рук – имеет следующий вид:

# define TACT 100

# define ON TRUE

# define OFF FALSE

# define STOP_STATE 0

# define ERROR_STATE 1

# define Ctrl_Waiting 2

# define Ctrl_Drying 3

value val;

int timer ;

int Ctrl_state ;

int Ctrl_timer ;

bool hands [];

bool dryer [];

inline void init () {

 timer = 0;

 Ctrl_state = Ctrl_Waiting ;

 Ctrl_timer = 0;

 ASSUME True ;

}

inline void Ctrl_exec () {

 switch ( Ctrl_state ) {

  case Ctrl_Waiting :

   if ( hands [ timer ] == ON) {

   dryer [ timer ] = ON;

   Ctrl_timer = 0;

   Ctrl_state = Ctrl_Drying ;

  }

else

  dryer [ timer ] = OFF;

  break ;

case Ctrl_Drying :

  if ( hands [ timer ] == ON) {

   Ctrl_timer = 0;

   Ctrl_state = Ctrl_Drying ;

  }

  if ( Ctrl_timer >= 10) {

   Ctrl_timer = 0;

   Ctrl_state = Ctrl_Waiting ;

  }

  break ;

 }

}

void main () {

 init ();

 for (;;) {

  INV lab inv;

  havoc hands [ timer ];

  ASSUME True ;

  Ctrl_exec ();

  Ctrl_timer = Ctrl_timer + 1;

  timer = timer + 1;

  hands [ timer ] = hands [timer -1];

  dryer [ timer ] = dryer [timer -1];

 }

}

Листинг 2: VOL-программа управления сушилкой для рук

Рассмотрим отношения между инструкциями исходной Reflex-программы и результирующей VOL-программы.

Макроконстанта TACT, специфицирующая время программного цикла, заменяет конструкцию TACT. Константы Reflex-программы (например, ON и OFF) также заменяются макроконстантами. Макроконстанты STOP_STATE и ERROR_STATE кодируют состояние останова (специфицирующее, что выполнение процесса на текущем такте завершается нормально) и состояние ошибки (специфицирующее, что выполнение процесса на текущем такте завершается с ошибкой). Для каждого программного процесса p_i и для каждого состояния s этого процесса, макроконстанта ${{p}_{i}}$_$s$ кодирует это состояние.

Переменные val, val₁, …, val_n рассматриваются как глобальные переменные VOL-программы типа value. В нашем случае, n = 0, так в программе не вычисляются функции и операции. Переменная timer специфицирует глобальный таймер. Для каждого программного процесса ${{p}_{i}}$, переменные ${{p}_{{i - }}}$state и ${{p}_{{i - }}}$timer специфицируют текущее состояние и локальный таймер процесса p_i. Тип t каждой Reflex-переменной x заменяется типом динамического массива t [].

Функция init() инициализирует процессы программы. Она устанавливает значение 0 для глобального таймера и всех локальных таймеров, устанавливает первый процесс в его начальное состояние и все остальные процессы в состояние останова и накладывает ограничения на начальные значения Reflex-переменных, используя аннотатор ASSUME  f (для программы управления сушилкой для рук ASSUME $True$).

Для каждого процесса p_i, функция ${{p}_{{i - }}}$exec специфицирует действия процесса p_i во время программного цикла. Тело функции ${{p}_{ - }}$exec представляет оператор switch, где метки – макроконстанты, кодирующие состояния процесса ${{p}_{{i - }}}$exec. Все специфические для языка Reflex операторы и операции в телах состояний процессов заменяются C-инструкциями в соответствие с их семантикой.

Бесконечный цикл for(;;), специфицирующий действия всех процессов во время программного цикла является последним оператором результирующей программы. Его тело начинается с инвариантного аннотатора INV $lab$ $inv$;, специфицирующего инвариант inv Reflex-программы. Следующий фрагмент

havoc hands[timer]; ASSUME True;

специфицирует внешние модификации Reflex-переменных (в нашем случае, hands) и ограничение True на них. Оператор havoc $x$;, добавленный в VOL из [28], моделирует присваивание произвольного значения переменной x из множества значений типа этой переменной. Третий фрагмент – это последовательность вызовов функций ${{p}_{{i - }}}$exec() для каждого процесса ${{p}_{i}}$. Следующий фрагмент увеличивает на 1 значения глобального таймера и всех локальных таймеров. Последний фрагмент специфицирует, что значения Reflex-переменных сохраняются после инкрементации глобального таймера, что соответствует переходу к новому такту выполнения Reflex-программы. Для программы управления сушилкой для рук, этот фрагмент имеет вид:

hands[timer] = hands[timer-1];

dryer[timer] = dryer[timer-1];.

В следующем разделе мы опишем общий вид правил трансляции Reflex-программ в VOL-программы (трансляционную семантику аннотированных Reflex-программ).

4. ТРАНСЛЯЦИОННАЯ СЕМАТИКА АННОТИРОВАННЫХ REFLEX-ПРОГРАММ

Пусть ${{C}_{R}}$ и ${{C}_{V}}$ – множество инструкций языков Reflex и VOL, соответственно. Программы на этих языках также включаются в эти множества. Пусть $C = {{C}_{R}} \cup {{C}_{V}}$. Трансляционная семантика языка Reflex задается бинарным отношением $ \rightsquigarrow \in C$ × C таким, что $\neg (c \rightsquigarrow c)$ для $c \in {{C}_{C}}$. Это отношение определяется правилами трансляции для Reflex-инструкций.

Программа. Для Reflex-программы p определим: $\{ {{p}_{1}},...,{{p}_{n}}\} $ – множество имен процессов; dec_T – декларация такта; $de{{c}_{c}}$, $de{{c}_{{v}}}$ и $de{{c}_{f}}$ – последовательности деклараций констант, переменных и внешних функций; m_i – число состояний процесса p_i; ${{s}_{{i1}}}, \ldots ,{{s}_{{i{{m}_{i}}}}}$ – последовательность имен состояний p_i в порядке их определения в программе p; $body({{s}_{{i{{k}_{i}}}}})$ – тело состояния ${{s}_{{i{{k}_{i}}}}}$, из которого исключены декларации переменных; $V = \{ {{{v}}_{1}},...,{{{v}}_{k}}\} $ – множество имен переменных программы p; V_e = = $\{ {{{v}}_{{e1}}},...,{{{v}}_{{es}}}\} \subseteq V$ – подмножество имен переменных, изменяемых объектом управления. Закодируем номера состояний процессов последовательными натуральными числами, начиная с 2 (коды 0 и 1 используются для состояний останова и ошибки). Пусть $num({{p}_{i}},{{s}_{{i{{k}_{i}}}}})$ – код состояния ${{s}_{{i{{k}_{i}}}}}$ процесса p_i. Тогда правило трансляции для p имеет вид:

$p \rightsquigarrow $

$de{{c}_{T}}$ $de{{c}_{c}}$

#define STOP_STATE 0

#define ERROR_STATE 1

#define ${{p}_{1}}$_${{s}_{{11}}}$ $num({{p}_{1}},{{s}_{{11}}})$

… // повторить для других состояний p₁

… // повторить для других процессов

value val; value val_1; value val_ $n$;

int timer;

int p_{1_state}; int ${{p}_{1}}$_timer

… // повторить для других процессов

$de{{c}_{v}}$ $de{{c}_{f}}$

inline void init() {

  timer = 0;

  p₁_state = p₁_${{s}_{{11}}}$; p₁_timer =0;

  ${{p}_{2}}$_state = STOP_STATE; ${{p}_{2}}$_timer =0;

  … // повторить для других процессов

  ASSUME icon;

}

$de{{c}_{1}}$ … $de{{c}_{n}}$

void main() {

   init();

   for (;;) {

   INV lab inv;

   havoc ${{{v}}_{{e1}}}$[timer];

   … // повторить для других переменных

   ASSUME econ;

   ${{p}_{1}}$_exec(); …; ${{p}_{n}}$_exec();

   ${{p}_{1}}$_timer = ${{p}_{1}}$_timer + 1;

   … // повторить для других процессов

   timer = timer + 1;

   ${{{v}}_{1}}$[timer] = ${{{v}}_{1}}$[timer-1];

   … // повторить для других переменных

 }

}

Здесь icon и econ – начальное и внешнее условия, соответственно; inv – инвариант программного цикла.

Определение dec_i функции ${{p}_{i}}$_exec, выполняющей процесс p_i в его текущем состоянии, имеет вид:

inline void ${{p}_{i}}$_exec {

  switch (${{p}_{i}}$_state) {

    case ${{p}_{i}}$_${{s}_{{i1}}}$: $body({{s}_{{i1}}})$ break;

    …

    case ${{p}_{i}}$_${{s}_{{i{{m}_{i}}}}}$: $body({{s}_{{i{{m}_{i}}}}})$ break;

  }

}

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

Правило подстановки. Правило подстановки позволяет применять правила трансляции к частям инструкций языка Reflex. Пусть c, c', c₁, ${{c}_{2}} \in C$, и $c[c{\text{'}}]$ обозначает место вхождения $c{\text{'}}$ в c. Тогда правило подстановки имеет вид:

Если ${{c}_{1}} \rightsquigarrow {{c}_{2}}$, то $c[{{c}_{1}}] \rightsquigarrow c[{{c}_{2}}]$.

Типы. Поскольку типы языка Reflex совпадают с типами языка VOL, правило трансляции для типов не требуется.

Декларация такта. Пусть k – число. Декларация такта определяется правилом:

TACT $k$; $ \rightsquigarrow $ #define TACT k.

Декларации констант. Пусть u – имя константы, $e$ – Reflex-выражение, и $\emptyset $ – пустой результат трансляции (удаление транслируемой инструкции). Декларации констант определяются правилами:

const $u$ $k$; $ \rightsquigarrow $ #define $u$ $k$

const $u$ $e$; $ \rightsquigarrow $ #define $u$ ($e$)

enum {${{u}_{1}}$, ${{u}_{2}}$, …} $ \rightsquigarrow $

  #define ${{u}_{1}}$ 0

  enum {${{u}_{2}}$ = 1, …}

enum {${{u}_{1}}$ = $k$, ${{u}_{2}}$, …} $ \rightsquigarrow $

    #define ${{u}_{1}}$ $k$

  enum {${{u}_{2}}$ = $k + 1$, …}

enum {} $\emptyset $

Декларации переменных. Декларации переменых определяются правилами:

$t$ $u$ ...; $ \rightsquigarrow $ $t$ $u$;

FROM PROC $pj$ $u$; $ \rightsquigarrow $ $\emptyset $.

Мы не учитываем в дедуктивной верификации связи переменных с портами и уровни доступа переменных. Поэтому, декларации Reflex-переменных непосредственно транслируются в декларации VOL-переменных.

Далее мы считаем, что Reflex-конструкции, для которых определяются правила, встречаются в теле некоторого состояния процесса p_i.

Операции над состояниями. Трансляционная семантика операций над состояниями определяется правилами:

(PROC IN STATE ACTIVE) $ \rightsquigarrow $

  (PROC ${{p}_{i}}$ IN STATE ACTIVE);

(PROC ${{p}_{j}}$ IN STATE ACTIVE) $ \rightsquigarrow $

  ((${{p}_{j}}$_state != STOP_STATE) &&

  (${{p}_{j}}$_state != ERROR_STATE));

(PROC IN STATE INACTIVE) $ \rightsquigarrow $

  (PROC ${{p}_{i}}$ IN STATE INACTIVE);

(PROC ${{p}_{j}}$ IN STATE INACTIVE) $ \rightsquigarrow $

  ((${{p}_{j}}$_state == STOP_STATE) ||

  (${{p}_{j}}$_state == ERROR_STATE));

(PROC IN STATE STOP) $ \rightsquigarrow $

  (PROC ${{p}_{i}}$ IN STATE STOP);

(PROC ${{p}_{j}}$ IN STATE STOP) $ \rightsquigarrow $

  (${{p}_{j}}$_state == STOP_STATE);

(PROC IN STATE ERROR) $ \rightsquigarrow $

  (PROC ${{p}_{i}}$ IN STATE ERROR);

(PROC ${{p}_{j}}$ IN STATE ERROR) $ \rightsquigarrow $

  (${{p}_{j}}$_state == ERROR_STATE).

Операторы управления состояниями. Операторы управления состояниями включают операторы STOP, ERROR, START, RESTART, SET и NEXT.

Оператор STOP определяется правилами:

STOP; $ \rightsquigarrow $ STOP PROC p_i;

STOP PROC ${{p}_{j}}$; $ \rightsquigarrow $

  {${{p}_{j}}$_timer=0; ${{p}_{j}}$_state= STOP_STATE;}.

Оператор ERROR определяется правилом:

ERROR; $ \rightsquigarrow $

   {${{p}_{i}}$_timer = 0; ${{p}_{i}}$_state = ERROR_ STATE;}.

Оператор START определяется правилом:

START PROC ${{p}_{j}}$; $ \rightsquigarrow $

{${{p}_{j}}$_timer = 0; ${{p}_{j}}$_state = ${{p}_{j}}$_${{s}_{1}}$;}.

Оператор RESTART определяется правилом:

RESTART $ \rightsquigarrow $ START PROC ${{p}_{i}}$;.

Оператор SET определяется правилом:

SET STATE ${{s}_{{ij}}}$; $ \rightsquigarrow $

{${{p}_{i}}$_timer = 0; ${{p}_{i}}$_state = ${{p}_{i}}$_${{s}_{{ij}}}$;}.

Оператор NEXT определяется правилом:

Если ${{p}_{i}}$_state = ${{s}_{{ij}}}$, то

SET NEXT; $ \rightsquigarrow $

{${{p}_{i}}$_timer = 0; ${{p}_{i}}$_state = ${{s}_{{i(j + 1)}}}$;}.

Операторы управления таймаутами. Операторы управления таймаутами включают операторы RESET и TIMEOUT.

Оператор RESET определяется правилом:

RESET TIMEOUT; $ \rightsquigarrow $ ${{p}_{i}}$_timer = 0;.

Пусть $st$ – Reflex-оператор. Оператор TIMEOUT определяется правилом:

TIMEOUT $e$ $st$ $ \rightsquigarrow $ if (${{p}_{i}}$_timer = $e$) $st$.

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

Таким образом, мы сводим верификацию временных свойств Reflex-программ к дедуктивной верификации VOL-программ. Дальше мы опишем правила порождения условий корректности для VOL-программ, примеры порожденных условий корректности для программы управления сушилкой для рук и их доказательство в SMT-решателе Z3.

5. ГЕНЕРАЦИЯ УСЛОВИЙ КОРРЕКТНОСТИ ДЛЯ C-ПРОЕКЦИЙ REFLEX-ПРОГРАММ

Подобно многим другим системам дедуктивной верификации, таким как FramaC [29], Spark [30], KeY [31], Dafny [32], и т.д., наш алгоритм порождения условий корректности определяет предикатный трансформер. Мы используем Z3 чтобы доказать порожденные условия корректности. Специфика алгоритма заключается в том, что он применяется к программе, которая является бесконечным циклом и некоторые переменные этой программы изменяются внешним образом на каждой итерации этого цикла. Алгоритм $sp(A,P)$ рекурсивно вычисляет сильнейшее постусловие [33], выраженное в многосортной логике первого порядка, для программного фрагмента A и предусловия P. Его применение начинается со всей программы и предусловия True. Результат его работы – множество условий корректности, сохраненное в переменной vcs. Алгоритм использует специальные переменные vars и $reached$. Переменная vars хранит информацию о переменных и их типах как множество пар вида x:t, где $x$ – переменная, а t – ее тип. Переменная $reached$ хранит множество имен инвариантных аннотаторов, которые были пройдены алгоритмом. Она используется чтобы гарантировать завершение алгоритма. Начальные значения этих переменных – пустые множества.

Мы определяем алгоритм порождения условий корректности sp как упорядоченное множество равенств вида $sp(A,P) = $ [${{a}_{1}}$; ...; ${{a}_{n}}$; $e$]. Эта нотация означает, что действия ${{a}_{1}}$, ..., ${{a}_{n}}$ последовательно выполняются перед тем, как выражение $e$ вычисляется. Каждое действие ${{a}_{i}}$ вида $v$ += $S$ добавляет элементы из множества $S$ в множество $v$. Равенство $sp(A,P) = e$ является сокращением для $sp(A,P) = $ [e].

Мы используем следующую нотацию в определении алгоритма. Пусть $array(t)$ обозначает тип массивов с элементами типа $t$. Пусть выражение $e$ имеет тип $t$, $\{ x{\text{:}}t,y{\text{:}}array(t)\} \subseteq vars$, {z:t, $v{\text{:}}t\} \cap $ ∩  vars = $\emptyset $ для каждого $t$, и $e{\text{'}}$ – результат преобразования VOL-выражения e в Z3py-выражение. Функция $Store(a,i,v)$ является функцией модификации массива из языка Z3.

В силу простоты языка VOL, алгоритм sp имеет следующую компактную форму:

1. $sp(t\,f({{t}_{1}}{{x}_{1}}, \ldots ,{{t}_{n}}{{x}_{n}})$;, $P) = $

    [$vars$ += $\{ {{x}_{1}}{\text{:}}{{t}_{1}}, \ldots ,{{x}_{n}}{\text{:}}{{t}_{n}},ret\_f{\text{:}}t\} ;P$];

2. $sp(t\,x;,P) = $ [$vars$ += $\{ x{\text{:}}t\} ;P$];

3. $sp($#define $ce$;$,P) = $

    [$vars$ += $\{ c:t\} $; $And(P,c = = e{\text{'}})$];

4. $sp($havoc $y$[$i$];$,P) = $

    [$vars$ += $\{ z{\text{:}}t,v{\text{:}}t\} $;

    $And(P(y \leftarrow z),y = = Store(z,i,v))$];

5. $sp($havoc $x$;$,P) = $

    [$vars$ += $\{ z{\text{:}}t\} $; $And(P(x \leftarrow z),x = = z)$];

6. $sp(x[i]$ = $e$; $,P) = $

    [$vars$ += $\{ z{\text{:}}array(t)\} $;

    $And(P(y \leftarrow z),y = = Store(z,i,e{\text{'}}(y \leftarrow z)))$];

7. $sp(x$ = $e$; $,P) = $

    [$vars$ += $\{ z{\text{:}}t\} $;

    $And(P(x \leftarrow z),x = = e{\kern 1pt} '(x \leftarrow z))$];

8. $sp(${$B$}$,P) = sp(B,P)$;

9. $sp($if ($e$) $B$ else $C,P) = $

    $Or(sp(B,And(P,econv(e))),$

    $sp(C,And(P,Not(econv(e))))$;

10. $sp($switch ($e$) ${{l}_{1}}$:${{B}_{1}}$ break; $ \ldots {{l}_{n}}$:${{B}_{n}}$ break; $,P) = $

    $Or(sp({{B}_{1}},And(P,e{\kern 1pt} ' = = {{l}_{1}})),$

    ...,

    $sp({{B}_{n}},And(P,e{\kern 1pt} ' = = {{l}_{n}})),$

    $And(P,e{\kern 1pt} '$ != ${{l}_{1}}, \ldots ,e{\kern 1pt} '$ != ${{l}_{n}}))$;

11. $sp($for(;;) {B}, P) $sp(B$ for(;;) {$B$}, $P)$;

12. $sp(f$(${{e}_{1}}$, ..., ${{e}_{n}})$; $,P) = $

       $sp({{e}_{1}}$; val_1 := val; $ \ldots {{e}_{n}}$; val_n := val;

           ASSERT ${{P}_{f}}[{{x}_{1}} \leftarrow $ val_1 $, \ldots ,{{x}_{n}} \leftarrow $ val_n];

           havoc val;

           ASSUME ${{Q}_{f}}[{{x}_{1}} \leftarrow $ val_1 $, \ldots ,{{x}_{n}} \leftarrow $ val_n]; , $P)$;

13. $sp({{e}_{1}}$ + ${{e}_{2}}$;$,P) = $

        $sp({{e}_{1}}$; val_1 := val; $ \ldots {{e}_{2}}$; val_2 := val;

val := (val_1 + val_2); $,P)$;

Другие операции определяются аналогичным образом. Заметим, что, для простоты, мы не рассматриваем приведение типов и считаем, что операции над числами в идеальной арифметике и машинной арифметике совпадают. Более точное определение операционной и аксиоматической семантик для операций может быть найдено в [34, 35].

14. $sp($ASSUME $e$; $,P) = And(P,e)$;

15. $sp($ASSERT $e$; $,P) = $

      [$vcs$ += $\{ \operatorname{Im} plies(P,e)\} $; $And(P,e)]$;

16. если $l \notin reached$, то $sp($INV $le$; $A,P) = $

      [$reached$ += {l}; $vcs$ += $\{ Implies(P,e)\} $; $sp(A,e)]$;

17. если $l \in reached$, то $sp($INV $le$; $A,P) = $

     [$vcs$ += $\{ Implies(P,e)\} $; $e]$;

18. $sp(stA,P) = sp(A,sp(st,P))$.

Этот алгоритм завершается, так как каждый вложенный вызов sp выполняется на меньшем программном фрагменте во всех случаях кроме for(;;) (случай 11), и, согласно случаю 16, алгоритм может проходить инвариантный аннотатор в начале тела цикла for(;;) только один раз.

Вычисление условий корректности для пути аннотированной программы, управляющей сушилкой для рук (Листинг 2), начинающегося в точке #define TACT 100 и заканчивающегося в точке INV lab inv; имеет в качестве результата:

• $vcs\, = \,\{ f\} $, где условие корректности  f  имеет вид:

     $Implies($

         And(True, TACT == 100, ON $ = = True,$

     OFF $ = = False,$ STOP_STATE $ = = 0,$

     ERROR_STATE == 1,

     Ctrl_Waiting == 2,

     Ctrl_Drying == 3, timer == 0,

     Ctrl_state == Ctrl_Waiting,

     Ctrl_timer == 0, dryer[0] == OFF,

     $True),$

         $inv)$;

• множество $vars$ включает следующие типизированные переменные и константы:

TACT:int, ON:bool, OFF:bool, val:value,

STOP_STATE:int, ERROR_STATE:int,

Ctrl_Waiting:int, Ctrl_Drying:int,

Ctrl_state:int, Ctrl_timer:int,

dryer:array(bool), hands:array(bool),

timer:int, timer_1:int,

Ctrl_state_1:int, Ctrl_timer_1:int;

• $reached = \{ lab\} $.

Другие семь условий корректности, начинающиеся в точке INV lab inv; и заканчивающиеся в той же самой точке и соответствующие различным ветвям оператора switch и операторов if, порождаются аналогичным образом. Все порожденные условия корректности успешно доказаны в Z3py.

Порождение условий корректности для VOL-программ – результатов трансляции аннотированных Reflex-программ – и их доказательство завершают описание нашего метода дедуктивной верификации Reflex-программ.

6. ЗАКЛЮЧЕНИЕ

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

Наш метод верификации имеет несколько отличительных свойств. Во-первых, он моделирует взаимодействие между Reflex-программой и управляемым ею объектом через входные и выходные порты, связанные с программными переменными. Инструкция havoc языка VOL позволяет моделировать запись значений из входных портов в программные переменные. Эти внешние значения переменных ограничиваются аннотатором ASSUME. Проверка значений, читаемых из программных переменных в выходные порты, специфицируется аннотаторами ASSERT и INVARIANT. Во-вторых, этот метод сводит верификацию ряда временных свойств Reflex-программ к дедуктивной верификации императивных программ за счет явного моделирования времени в VOL-программах – результатах трансляции Reflex-программ – с помощью глобальных и локальных таймеров, а также историй значений Reflex-переменных, представленных массивами. В-третьих, наш алгоритм порождения условий корректности может применяться к бесконечным циклам, свойственным системам управления.

Имеются несколько направлений для дальнейшего развития метода. Мы планируем расширить его на текстовые языки стандарта IEC 61131-3. Подобно языку Reflex, эти языки используются для программ, которые взаимодействуют с объектом управления только между программными циклами.

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

Явное моделирование времени в Reflex-аннотациях не очень удобный способ описания временных свойств Reflex-программ. Мы планируем использовать временные логики (LTL, CTL and MTL) и их расширения чтобы описывать эти свойства более естественным образом и разработать алгоритм трансляции таких описаний в формулы с явным моделированием времени. Чтобы сделать эту задачу выполнимой, мы планируем использовать специализированные онтологические паттерны [36] вместо произвольных формул этих логик.

В дополнение к решателю Z3 мы намерены использовать другие средства машинной поддержки доказательства чтобы расширить класс проверяемых свойств. В частности, решатель Z3 не смог доказать свойство, что сушилка будет работать в течение не менее 10 секунд после удаления рук, поскольку это свойство требует расширенной индукции. Интерактивный доказатель теорем ACL2 [37] с более развитыми индукционными схемами является хорошим кандидатом для решения этой проблемы.

Чтобы упростить доказательство корректности алгоритмов трансляции и порождения условий корректности, мы планируем использовать унифицированное графо-онтологическое представление для программ на языках Reflex и VOL. Такое представление позволяет свести трансляционную семантику к трансформационной в рамках одного общего графо-онтологического языка и применить онтологический подход для разработки операционной семантики этих языков [38].