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

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 43 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 2 2021 моделирующей поведение. Инва- рианты доказываются как теоремы. Доказательство теорем гарантирует соответствие требованиям. Платфор- ма Rodin ускоряет и упрощает дока- зательства теорем, а также исключа- ет их ошибочность. Формальный дедуктивный анализ хорошо сочетается с автоматным про- ектированием алгоритмов: для форма- лизации алгоритма не требуется допол- нительных преобразований, так как автоматы уже представляют собой математические объекты. Литература 1. Нейзов М. Формальный дедуктивный ана- лиз автоматного алгоритма управления генератором эндогаза с помощью плат- формы Rodin. Часть 1. Определение тре- бований надежности и безопасности работы генератора эндогаза. Современ- ная электроника. 2020. № 9. 2. Нейзов М. Формальный дедуктивный ана- лиз автоматного алгоритма управления генератором эндогаза с помощью плат- формы Rodin. Часть 2. Алгоритм управ- ления и платформа Rodin. Современная электроника. 2021. № 1. Таблица 2. Основные леммы теоремы Т16 Лемма Утверждение lem1 LA_y3(dta(a ↦ (x1 ↦ x2 ↦ x3)))=TRUE ∧ LA_y1(dta(a ↦ (x1 ↦ x2 ↦ x3)))=TRUE ∧ LB_y1(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∧ LB_y3(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∧ (LB_y5(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∨ LB_y6(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE) ⇒ (dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))=B6 ∨ dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))=B8) Интерпретация: V1=TRUE ∧ K1=TRUE ∧ V3=TRUE ∧ V5=TRUE ∧ (V7=TRUE ∨ V8=TRUE) ⇒ (b=B6 ∨ b=B8) lem1.1 ¬dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)) ∈ {B1,B2,B3,B4,B5, B7,B9} lem2 (dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))=B6 ∨ dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))=B8) ⇒ LA_y3(dta(a ↦ (x1 ↦ x2 ↦ x3)))=TRUE ∧ LA_y1(dta(a ↦ (x1 ↦ x2 ↦ x3)))=TRUE ∧ LB_y1(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∧ LB_y3(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∧ (LB_y5(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∨ LB_y6(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE) Интерпретация: (b=B6 ∨ b=B8) ⇒ V1=TRUE ∧ K1=TRUE ∧ V3=TRUE ∧ V5=TRUE ∧ (V7=TRUE ∨ V8=TRUE) lem2.1 LA_y3(dta(a ↦ (x1 ↦ x2 ↦ x3)))=TRUE Интерпретация: V1=TRUE lem2.1.1 dta(a ↦ (x1 ↦ x2 ↦ x3))=A2 lem2.2 LA_y1(dta(a ↦ (x1 ↦ x2 ↦ x3)))=TRUE Интерпретация: K1=TRUE lem2.3 LB_y1(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE Интерпретация: V3=TRUE lem2.3.1 dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)) ∈ {B2,B4,B6,B7,B8} lem2.4 LB_y3(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE Интерпретация: V5=TRUE lem2.4.1 dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)) ∈ {B2,B5,B6,B8,B9} lem2.5 (LB_y5(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE ∨ LB_y6(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)))=TRUE) Интерпретация: (V7=TRUE ∨ V8=TRUE) Автоматизация Автомобилестроение Медицина Особенности: