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

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 62 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 9 2020 Формальный дедуктивный анализ автоматного алгоритма управления генератором эндогаза с помощью платформы Rodin Часть 1. Определение требований надёжности и безопасности работы генератора эндогаза Рис. 1. Схема генератора эндогаза Формальный дедуктивный анализ представляет собой строгий математический подход к верификации алгоритмов: алгоритм описывается с помощью аксиом, а требуемые свойства доказываются как теоремы. Цель представленного анализа – доказать соответствие алгоритма управления предъявляемым требованиям надёжности и безопасности. В статье описывается технологический процесс генерации эндогаза и определяются предъявляемые к нему требования надёжности и безопасности. Максим Нейзов (neyzov.max@gmail.com ) Введение Кпрограммному обеспечениюответ- ственных систем управления предъяв- ляются серьёзные требования по без- опасности. Для гарантии соответствия программ требованиям применяются формальные методы верификации и специальные инструментальные сред- ства. В статье представленформальный дедуктивный анализ автоматного алго- ритма управления на предмет его соот- ветствия требованиям безопасности технологического процесса генерации эндогаза. Данный анализ представляет собой строгийматематический подход к исследуемой проблеме: математиче- скаямодель алгоритма строится на базе системы аксиом, а свойства безопасно- сти доказываются как теоремы. Платфор- ма Rodin [1] используется как средство автоматизации доказательства теорем. В первой части статьи определя- ются требования надёжности и безо- пасности технологического процесса. Во второй – представлена платфор- ма Rodin и автоматный алгоритм управления генератором. В третьей – выполняется построение формаль- ной теории для алгоритма управле- ния: алгоритм описывается с помощью аксиом, формализуются требования, которые должны быть доказаны как теоремы, демонстрируется доказа- тельство теоремы. Технологический процесс генерации эндогаза Эндогаз используется в промышлен- ной термообработке для насыщения стали углеродом. Эндогазовая установ- ка предназначена для получения эндога- за. Химическая реакция приготовления эндогаза осуществляется в генераторе, который входит в состав установки. Схе- ма генератора эндогаза изображена на рисунке 1. Генерация эндогаза имеет сле- дующуютехнологию: исходная газовоз- душная смесь (далее газ) проходит через катализатор ретортыипод воздействием температуры+1050°С в результате хими- ческой реакции преобразуется в эндо- газ. Далее происходит его охлаждение в холодильнике. Генераторимеет два кана- ла: канал ретортыR1и канал ретортыR2. Вработе может находиться только один канал, второй канал –на восстановлении катализатора. Восстановление осущест- вляется чистымвоздухом. Перед генера- циейреторта должна продуваться газом в течении определённого времени. В компрессорный блок входят ком- прессоры К1, К2 и клапаны V1, V2. Для подачи газа в реторты R1/R2 открыва- ется клапан V1 и включается компрес- сор К1, создавая давление в линии Л1. Для подачи воздуха в реторты R1/R2 включается компрессор К2, создавая давление в линии Л2. При поломке ком- прессора К2 генерация эндогаза пре- кращается, и продувка реторт воздухом осуществляется с помощью компрессо- ра К1. Для этого закрывается клапан V1 и открывается клапан V2. Клапаны реторт V3…V10 предназна- чены для управления потоками через реторты R1/R2. Клапаны V4 и V6 пред- назначены для подачи воздуха в ретор- ты. Клапаны V3 и V5 предназначены для подачи газа в реторты, а также воздуха в случае отказа компрессора К2. Клапа- ны V7 и V8 предназначены для подачи горячего эндогаза в линию Л3. Клапа- ны V9 и V10 предназначены для про- дувки реторт на свечу.