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

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 40 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 2 2021 Формальный дедуктивный анализ автоматного алгоритма управления генератором эндогаза с помощью платформы Rodin Часть 3. Построение формальной теории для алгоритма управления Формальный дедуктивный анализ представляет собой строгий математический подход к верификации алгоритмов: алгоритм описывается с помощью аксиом, а требуемые свойства доказываются как теоремы. Цель представленного анализа – доказать соответствие алгоритма управления предъявляемым требованиям надежности и безопасности. В статье выполнено построение формальной теории для алгоритма управления: проведена аксиоматизация алгоритма, формализованы требования, продемонстрировано доказательство теоремы с помощью платформы Rodin. Максим Нейзов (neyzov.max@gmail.com ) Введение В предыдущих частях статьи были определены требования надёжности и безопасности [1], предъявляемые к алго- ритму, рассмотрены автоматный алго- ритм управления и платформа Rodin [2]. В настоящей работе для верификации алгоритма выполняется формальный дедуктивный анализ, который состоит в построенииформальной аксиоматиче- ской теории. Для этого алгоритм описы- вается с помощью аксиом, выполняется формализация требований и проводит- ся автоматизированное доказательство теорем с помощью платформы Rodin. Аксиоматика автоматов Автоматы A и B [2] задаются с помо- щью аксиом в контексте (см. листинг 1 и 2 соответственно). Назначение акси- ом представлено в таблице 1. Если акси- оматика противоречива, то модель не может быть запущена на исполнение. Динамическая модель алгоритма и окружения Аксиомы контекста задают статиче- скуючасть модели, машина задает дина- мическую часть [2]. Машина моделиру- ет поведение СВА. Вмашине объявлены переменные и событие iter (см. листинг 3), изменяющее состояние машины. Событие может возникнуть с любыми параметрами x1…x5, удовлетворяю- щими охранным условиям grd1…grd7. Охранные условия grd1…grd7 модели- руют поведение окружения автома- тов. Условия grd1…grd5 ограничивают тип параметров x1…x5. СВА имеет пять входов булевого типа. Условия grd6, grd7 ограничивают значения параметров x2, x3. Данные ограничения обусловлены работой блоков f_RzG и f_RzK2. Собы- тие iter изменяет состояние машины, выполняя действия act1…act20. Действие act1 изменяет переменную a – текущее состояние автомата А, вызывая егофунк- циюпереходов dta. Действия act2…act5 изменяют выходы автомата А, вызывая егофункции выходов LA_y1…LA_y4. Дей- ствие act6 изменяет переменную b – текущее состояние автомата B, вызы- вая его функцию переходов dtb. Дей- ствия act7…act15 изменяют выходы автомата B, вызывая егофункции выхо- дов LB_y1…LB_y9. Действия act16…act20 сохраняют значения параметров x1…x5 в соответствующие им переменные. Формализация требований Требования надёжности и безопас- ности REQ1 … REQ16 [1] в виде матема- тических утверждений T1 … T16 записы- ваются в разделе инвариантов машины (см. листинг 4) и должны быть доказа- ны как теоремы. Теоремы Т1 … Т5 утверждают, что ука- занные клапаны никогда не открыты одновременно ( REQ1 … REQ5 ). Теорема Т6 утверждает, что для любо- го клапана v, принадлежащего множе- ству клапанов Valve = {v i | i=1…10}, при снятии сигнала Run клапан v закрыва- ется ( REQ6 ). Теоремы Т7 , Т8 утверждают, что ком- прессоры работают только при нали- чии соответствующих разрешений ( REQ7 , REQ8 ). Теорема Т9 утверждает, что при рабо- те компрессора К2 клапан V2 всегда закрыт – это гарантирует, что воздуш- ный компрессор К2 перекачивает толь- ко воздух ( REQ9 ). Теорема Т10 утверждает, что при работе компрессора К1 всегда открыт только один из клапанов V1 или V2 – это гарантирует, что компрессор К1 Листинг 1 axm1: partition(A, {A1},{A2},{A3},{A4}) axm2: InA = (BOOL × BOOL × BOOL) axm3: a_1_2 = {x1 ↦ x2 ↦ x3 | x1=TRUE ∧ x2=TRUE ∧ x3=TRUE} axm4: a_2_3 = {x1 ↦ x2 ↦ x3 | x1=TRUE ∧ x2=TRUE ∧ x3=FALSE} axm5: a_2_4 = {x1 ↦ x2 ↦ x3 | x1=TRUE ∧ x2=FALSE ∧ x3=TRUE} axm6: a_234_1 = {x1 ↦ x2 ↦ x3 | (x1=FALSE ∧ x2 ∈ BOOL ∧ x3 ∈ BOOL) ∨ (x1 ∈ BOOL ∧ x2=FALSE ∧ x3=FALSE)} axm7: a_1_1 = InA\(a_1_2) axm8: a_2_2 = InA\(a_2_3 ∪ a_2_4 ∪ a_234_1) axm9: a_3_3 = InA\(a_234_1) axm10: a_4_4 = InA\(a_234_1) axm11: dta ∈ (A × InA) → A axm12: ∀ s,i•((s=A1 ∧ i ∈ a_1_1) ∨ (s ∈ {A2,A3,A4} ∧ i ∈ a_234_1)) ⇔ dta(s ↦ i) = A1 axm13: ∀ s,i•((s=A1 ∧ i ∈ a_1_2) ∨ (s=A2 ∧ i ∈ a_2_2)) ⇔ dta(s ↦ i) = A2 axm14: ∀ s,i•((s=A2 ∧ i ∈ a_2_3) ∨ (s=A3 ∧ i ∈ a_3_3)) ⇔ dta(s ↦ i) = A3 axm15: ∀ s,i•((s=A2 ∧ i ∈ a_2_4) ∨ (s=A4 ∧ i ∈ a_4_4)) ⇔ dta(s ↦ i) = A4 axm16: LA_y1 ∈ A → BOOL axm17: LA_y2 ∈ A → BOOL axm18: LA_y3 ∈ A → BOOL axm19: LA_y4 ∈ A → BOOL axm20: ∀ s•(s=A2 ∨ s=A3) ⇔ LA_y1(s) = TRUE axm21: ∀ s•(s=A2 ∨ s=A4) ⇔ LA_y2(s) = TRUE axm22: ∀ s•(s=A2) ⇔ LA_y3(s) = TRUE axm23: ∀ s•(s=A3) ⇔ LA_y4(s) = TRUE