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

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 42 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 2 2021 доказательства леммы lem2.1 . Лемма lem2.1.1 утверждает, что функция dtа при принятых гипотезах всегда возвра- щает значение А2. Доказательство лем- мы lem2.1.1 основывается на том, что если функция dtb возвращает значе- ние B6 или B8, то функция dta не может вернуть ничего кроме А2. Если автомат А находится в состоянии А2, то LA_y3 имеет значение TRUE (согласно аксио- ме axm22 ), что и требовалось доказать в лемме lem2.1 . Лемма lem2.2 утверждает, что функ- ция выходов LA_y1 имеет значение TRUE. Для доказательства этой леммы используется уже доказанная лемма lem2.1.1 и аксиома axm20 . Лемма lem2.3 утверждает, что функ- ция выходов LB_y1 имеет значение TRUE. Лемма lem2.3.1 использует- ся для доказательства леммы lem2.3 . Лемма lem2.3.1 утверждает, что функ- ция dtb при принятых гипотезах всегда возвращает значения, при- надлежащие множеству {B2, B4, B6, B7, B8}. Если автомат B находится в одном из перечисленных состоя- ний, то LB_y1 имеет значение TRUE (согласно аксиоме axm65 ), что и тре- бовалось доказать в лемме lem2.3 . Лемма lem2.4 имеет аналогичное доказательство. Лемма lem2.5 утверждает, что функ- ция выходов LB_y5 или LB_y6 имеет зна- чение TRUE. В ветке доказательства лем- мы lem2 принята следующая гипотеза: функция dtb возвращает значение B6 или B8. Если функция dtb возвращает значение B6, то функция LB_y5 име- ет значение TRUE (согласно аксиоме axm69 ), если функция dtb возвращает значение B8, то функция LB_y6 име- ет значение TRUE (согласно аксиоме axm70 ), что и требовалось доказать в лемме lem2.5 . Таким образом, дока- зательство всех перечисленных лемм доказывает теорему Т16 . Леммы lem1.1 , lem2.1.1 , lem2.3.1 , lem2.4.1 были добав- лены в дерево доказательства вручную, остальные леммы таблицы 2 были сге- нерированы программой-прувером автоматически. Заключение В статье рассмотрен алгоритм управления генератором эндога- за, спроектированный как СВА. Для обеспечения надёжности и безопас- ности технологического процесса алгоритм должен гарантированно соответствовать ряду требований. Для доказательства соответствия требованиям выполняется формаль- ный дедуктивный анализ. С помощью платформы Rodin строится матема- тическая модель алгоритма и его окружения. Требования подлежат формализации. Каждое требование задаётся как инвариант машины, Листинг 3 iter ANY x1 x2 x3 x4 x5 WHERE grd1: x1 ∈ BOOL grd2: x2 ∈ BOOL grd3: x3 ∈ BOOL grd4: x4 ∈ BOOL grd5: x5 ∈ BOOL grd6: (a = A3) ⇒ (x2 = TRUE ∧ x3 = FALSE) grd7: (a = A4) ⇒ (x2 = FALSE ∧ x3 = TRUE) THEN act1: a ≔ dta(a ↦ (x1 ↦ x2 ↦ x3)) act2: K1 ≔ LA_y1(dta(a ↦ (x1 ↦ x2 ↦ x3))) act3: K2 ≔ LA_y2(dta(a ↦ (x1 ↦ x2 ↦ x3))) act4: V1 ≔ LA_y3(dta(a ↦ (x1 ↦ x2 ↦ x3))) act5: V2 ≔ LA_y4(dta(a ↦ (x1 ↦ x2 ↦ x3))) act6: b ≔ dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5)) act7: V3 ≔ LB_y1(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act8: V4 ≔ LB_y2(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act9: V5 ≔ LB_y3(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act10: V6 ≔ LB_y4(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act11: V7 ≔ LB_y5(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act12: V8 ≔ LB_y6(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act13: V9 ≔ LB_y7(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act14: V10 ≔ LB_y8(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act15: tmrQ ≔ LB_y9(dtb(b ↦ (dta(a ↦ (x1 ↦ x2 ↦ x3)) ↦ x4 ↦ x5))) act16: Run ≔ x1 act17: RzG ≔ x2 act18: RzK2 ≔ x3 act19: sw1 ≔ x4 act20: tmrI ≔ x5 END Листинг 4 INVARIANTS ... T1: ¬(V1=TRUE ∧ V2=TRUE) T2: ¬(V3=TRUE ∧ V4=TRUE) T3: ¬(V5=TRUE ∧ V6=TRUE) T4: ¬(V7=TRUE ∧ V9=TRUE) T5: ¬(V8=TRUE ∧ V10=TRUE) T6: ∀ v•(v ∈ Valve ∧ Run=FALSE) ⇒ closed(v)=TRUE T7: K1=TRUE ⇒ RzG=TRUE T8: K2=TRUE ⇒ RzK2=TRUE T9: K2=TRUE ⇒ V2=FALSE T10: K1=TRUE ⇒ ((V1=TRUE ∧ V2=FALSE) ∨ (V2=TRUE ∧ V1=FALSE)) T11: (K1=TRUE ∧ K2=TRUE) ⇒ V2=FALSE T12: (Run=FALSE) ⇒ (K1=FALSE ∧ K2=FALSE) T13: ¬(V7=TRUE ∧ V8=TRUE) T14_1: ¬((V7=TRUE ∧ V9=TRUE) ∨ (V7=TRUE ∧ V4=TRUE) ∨ (V7=TRUE ∧ V3=TRUE ∧ V2=TRUE)) T14_2: ¬((V8=TRUE ∧ V10=TRUE) ∨ (V8=TRUE ∧ V6=TRUE) ∨ (V8=TRUE ∧ V5=TRUE ∧ V2=TRUE)) T15: (K1=TRUE ∧ V1=TRUE) ⇒ ((V3=TRUE ∧ (V7=TRUE ∨ V9=TRUE)) ∨ (V5=TRUE ∧ (V8=TRUE ∨ V10=TRUE))) T16: (V1=TRUE ∧ K1=TRUE ∧ V3=TRUE ∧ V5=TRUE ∧ (V7=TRUE ∨ V8=TRUE)) ⇔ (b=B6 ∨ b=B8) Рис. 1. Дерево доказательства теоремы Т16