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

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 45 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 1 2021 Рис. 3. Граф переходов автомата А ские утверждения можно переформу- лировать на языке теории множеств [2]. Одной из главных концепций метода Event-B является уточнение [3–6]. Слож- ные системы строятся как последова- тельность уточнений. Каждое уточ- нение добавляет некоторые детали и конкретизирует систему. Таким обра- зом, осуществляется последователь- ное движение от абстрактного к кон- кретному. В Event-B существует два вида компонентов: контекст и маши- на [3–6]. Контекст задаёт статическую часть модели, машина – динамическую. Аксиомы задаются в контексте. Маши- не доступна вся информация из ука- занного контекста. Машина содержит переменные, отвечающие за текущее состояние, и события , действия кото- рые изменяют значения переменных. События могут иметь параметры и охранные условия . Событие может произойти, только если его параме- тры удовлетворяют охранным услови- ям. Если охранные условия позволяют произойти сразу нескольким событи- ям, то случайным образом выбирается одно из них. Таким образом, построен- ная модель определяет недетерминиро- ванную дискретную систему переходов [3, 5]. В машине объявляются инвариан- ты – утверждения, истинные в любом её состоянии. Инварианты включаются в список обязательств по доказатель- ству [3] и должны быть доказаны, как и теоремы. Теоремы могут быть объяв- лены как в контексте, так и в машине. При доказательстве теорем в интерак- тивном режиме могут применяться раз- личные тактики . Возможно добавле- ние произвольных гипотез , которые становятся леммами после их доказа- тельства. Автоматный подход к разработке алгоритмов Автоматное программирование [7] – концепция разработки алгоритмов, управляющая часть которых проек- тируется как система взаимосвязан- ных автоматов (СВА) [8]. Алгоритмы управления чаще всего состоят толь- ко из управляющей части и представ- ляют собой СВА. Автомат является преобразователем входных последо- вательностей сигналов в выходные [2, 9]. Выходной сигнал зависит от вход- ного сигнала и состояния автомата, хронящего предысторию всех входных сигналов. Автоматный подход позволя- ет избежать ряда ошибок и способству- ет построению более надёжных и без- опасных алгоритмов управления [10]. Автоматный подход к разработке алго- ритмов получил широкое распростра- нение [7, 8, 10–16]. Автоматы удобно задавать в виде графов переходов . Для формального дедуктивного ана- лиза алгоритма необходимо его пред- ставление в строгой математической форме. Автоматный подход проектиро- вания в данном случае является очень удобным, так как автомат уже являет- ся строгим математическим объектом. Не требуется никаких дополнительных преобразований. Автоматный алгоритм управления Алгоритм управления генератором эндогаза представлен как СВА, состо- ящая из двух автоматов – A и B. Авто- мат A управляет компрессорным бло- ком, автомат B – клапанами реторт. Интерфейсы автоматов представлены на рисунках 1 и 2. Автомат A имеет три входа и четыре выхода, а автомат B – три входа и девять выходов. Блок f_RzG устанавливает сигнал, если выполняет- ся условие: ¬P1min ∧ ¬P1max ∧ water ∧ ¬Fail_K1. Блок f_RzK2 устанавливает сиг- нал, если выполняется условие: ¬Fail_ K2. Если заданное условие не выпол- няется, то блок сбрасывает выходной сигнал. Для повторной установки сиг- нала требуется перезапуск блока перед- ним фронтом сигнала Run. Автомат B использует текущее состояние автомата A для управления. Автомат B взаимодей- ствует с таймером для выдержки задан- ного интервала времени. Графы переходов автоматов явля- ются полной и точной специфика- цией их поведения (представлены на рисунках 3 и 4). A и B – автоматы Мура [2, 7–9]. Состояния А1 и В1 – началь- ные. В левом верхнем углу вершин графа указаны состояния автомата, в правом верхнем углу – коды дей- ствий автомата, внизу – установлен- ные сигналы. Таким образом, в состо- янии А4 компрессор К1 остановлен, а компрессор К2 перекачивает воздух, для этого установлен один выходной сигнал К2, остальные сигналы сброше- ны. Если условия на всех дугах, исхо- дящих из состояния, ложны, то авто- мат остаётся в прежнем состоянии. Если в состояние можно перейти из других состояний по одному и тому же условию, то происходит объедине- ние в группу (обрамляется пунктиром) и указывается один переход из данной группы. Таким образом, из состояний А2…А4 можно перейти в состояние А1 по указанному условию. При наличии сигнала Run и разреше- ний RzG и RzK2 автомат А переходит из состояния А1 в состояние А2. При этом включаются компрессоры К1, К2 и открывается клапан V1. Переход автомата А в состояние А2 приводит к переходу автомата B из состояния B1 в состояние B4 (при наличии сигнала sw1). Состоянию B4 соответствует про- дувка реторты R1 газом, а также ретор- ты R2 воздухом. При этом открываются клапаны V3, V6, V9, V10 и устанавлива- ется сигнал tmrQ для запуска таймера продувки реторты. После окончания времени продувки таймер устанавли- вает сигнал tmrI и автомат B переходит в состояние B7. Состоянию B7 соответ- ствует работа реторты R1 и продувка реторты R2 воздухом. При этом клапан V9 закрывается, а клапан V7 открывает- ся, остальные клапаны остаются в преж- нем положении. При исчезновении разрешения генерации RzG автомат А перехо-