Современная электроника №1/2021

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 44 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 1 2021 Формальный дедуктивный анализ автоматного алгоритма управления генератором эндогаза с помощью платформы Rodin Часть 2. Алгоритм управления и платформа Rodin Рис. 1. Интерфейс автомата А Рис. 2. Интерфейс автомата В Формальный дедуктивный анализ представляет собой строгий математический подход к верификации алгоритмов: алгоритм описывается с помощью аксиом, а требуемые свойства доказываются как теоремы. Цель представленного анализа – доказать соответствие алгоритма управления предъявляемым требованиям надёжности и безопасности. В статье представлен алгоритм управления в виде системы взаимосвязанных автоматов и платформа Rodin – инструмент для формального анализа систем и автоматизации доказательства теорем. Максим Нейзов (neyzov.max@gmail.com ) Введение: формальные аксиоматические теории В первой части статьи [1] были опре- делены требования надёжности и безо- пасности технологического процесса. Для гарантии соответствия алгоритма данным требованиям необходим его формальный анализ, который будет состоять в построении формальной аксиоматической теории. Аксиоматический способ построе- ния теории был известен ещё до нашей эры и применён Евклидом в геометрии. Аксиоматические теории – это теории, в основе которых лежит набор аксиом и правил вывода. Аксиомы – элемен- тарные утверждения, принимаемые без доказательств. Теоремы – утверждения, имеющие доказательства. Доказатель- ство – цепочка логических рассужде- ний, которая строится с помощью пра- вил вывода, аксиом и уже доказанных теорем [2]. Таким образом, теорема – это логическое следствие из аксиом. Метод получения нового знания явля- ется дедуктивным . Теория интерес- на, прежде всего, как множество тео- рем. Полученные знания достоверны, если доказательства теорем не содер- жат ошибок. Для исключения ошибок строятся формальные теории . Форма- лизация теории – это её построение с помощью строгого математическо- го аппарата. Все объекты и действия в формальной теории строго фикси- рованы. Формальное доказательство представляет собой легко проверяемую (в том числе и компьютерной програм- мой) цепочку формул. Для гарантии соблюдения заданных требований выполняется формальный дедуктивный анализ алгоритма управ- ления. Строится формальная аксиома- тическая теория алгоритма. Алгоритм представляется с помощью набора аксиом. Теоремы представляют свой- ства данного алгоритма. Доказанное свойство является атрибутом алгорит- ма по построению, так как оно логи- чески следует из него. Если теорема доказана, то алгоритм гарантирован- но обладает данным свойством. Если алгоритм не обладает данным свой- ством, то свойство не является теоре- мой данной теории, следовательно, не существует цепочки рассуждений для доказательства. После доказательства наличия заданного свойства у алго- ритма нет смысла в его тестировании с целью поиска контрпримеров, нару- шающих это свойство. Так же бес- смысленно, как после доказательства теоремы Пифагора пытаться найти прямоугольный треугольник, наруша- ющий равенство: a 2 + b 2 = c 2 , где a, b – катеты, c – гипотенуза. Платформа Rodin Платформа Rodin [3] – инструмен- тальное программное обеспечение, предназначенное для поддержки мето- да Event-B [4–6]. Event-B – формаль- ный метод моделирования и анализа систем. Платформа Rodin имеет множе- ство плагинов и позволяет редактиро- вать модели, запускать на исполнение для валидации и тестирования, выпол- нять проверку модели (model checking), доказывать простые теоремы автома- тически и теоремы любой сложности в интерактивном режиме. Для моделирования в Event-B исполь- зуются теория множеств и логика пре- дикатов [5]. Язык множеств является универсальным: любые математиче-