Event-B Доказательства Обязательства

Question

У меня в Event-B проблема с выполнением доказательств. В своей работе я хочу формализовать спецификацию требований защиты памяти, чтобы проверить их соответствие. Чтобы сделать это, я использовал Event-B Context для формализации структуры системы и использовал Event-B Machine для описания требований. Каждое требование описано как в Инварианте, так и в Событии. Событие-B проверит каждую пару требований, чтобы найти несоответствие.
Тем не менее, он не может доказать, что два требования согласованы: 1: "Доступ начтение из NonTrusted к разделу data_Apps других OS_Apps - may_prevent"
2: "Доступ начтение и запись из OS_App к его собственному разделу data_permit"

Это моя работа. Во-первых, в файле контекста я опишу структуру системы и контроль доступа:
1. Структура системы:
У нас есть 2 типа OS_Application: доверенные и ненадежные.
2 типа объектов OS_Object: задачи и ISR.
2 типа ISR: Категория_1 и Категория_2.
Каждый OS_Object принадлежит одному OS_App: ContainerOf ∈ OS_Obj → OS_App
Каждое OS_App имеет раздел кода: AppCode ∈ OS_App → CodeSection
Память состоит из 2 частей: DataSection и Stack
OS_App и OS_Obj могут иметь DataSection:

• AppData ∈ OS_App ⇸ DataSecs
• ObjData ∈ OS_Obj ⇸ DataSecs

OS_Obj имеет свой собственный стек: ObjStack ∈ OS_Obj → Стеки

2. Контроль доступа:
Доступ осуществляется от субъектов к объектам:
Темы включают в себя: OS_App и OS_Obj
Объекты включают: Code_Section и Memory
В приведенном ниже коде строка 20 описывает: "Стек для этих объектов по определению принадлежит только объекту-владельцу, и поэтому нет необходимости совместно использовать данные стека между объектами, даже если эти объекты принадлежат одному и тому же OS-приложению."

строка 21 описывает: "Разделы кода либо являются частными для OS-приложения, либо могут использоваться всеми OS-приложениями"
Строки 22, 23 описывают: "Приложения OS могут иметь частные разделы данных, а задачи /ISR могут иметь частные разделы данных".
строка 24 описывает: "Частные разделы данных OS-приложения совместно используются всеми задачами /ISR, принадлежащими этому OS-приложению".

По анализу я определяю контекст следующим образом:

1:  OS_Obj ⊆ Subjects   
2:  OS_App ⊆ Subjects ∖ OS_Obj
3:  Tasks ⊆ OS_Obj
4:  ISRs ⊆ OS_Obj∖Tasks
5:  Category_1_ISRs ⊆ ISRs
6:  Category_2_ISRs = ISRs ∖ Category_1_ISRs
7:  Trusted_OS ⊆ OS_App
8:  NonTrusted_OS = OS_App ∖ Trusted_OS
9:  CodeSection ⊆ Objects
10: Memory ⊆ Objects ∖ CodeSection
11: DataSecs ⊆ Memory
12: Stacks ⊆ Memory ∖ DataSecs
13: partition(actions_set, {initact}, {read}, {write}, {execute})
14: partition(status_set, {initStt}, {shall_prevent}, {shall_permit}, {may_prevent}, {may_permit})
15: ObjData ∈ OS_Obj ⇸ DataSecs
16: ObjStack ∈ OS_Obj → Stacks
17: AppCode ∈ OS_App → CodeSection
18: AppData ∈ OS_App ⇸ DataSecs
19: ContainerOf ∈ OS_Obj → OS_App 
20: ∀obj1,obj2 · (obj1 ∈ OS_Obj ∧ obj2 ∈ OS_Obj ∧ (obj1 ≠ obj2) ⇒ (ObjStack(obj1) ≠ ObjStack(obj2)))
21: ∀app1, app2 · (app1 ∈ OS_App ∧ app2 ∈ OS_App ∧ app1 ≠ app2) ⇒ AppCode(app1) = AppCode(app2)
22: ∀app1, app2 · (app1 ∈ dom(AppData) ∧ app2 ∈ dom(AppData) ∧ app1 ≠ app2) ⇒ AppData(app1) ≠ AppData(app2)
23: ∀ obj1, obj2 · (obj1 ∈ dom(ObjData) ∧ obj2 ∈ dom(ObjData) ∧ obj1 ≠ obj2) ⇒ ObjData(obj1) ≠ ObjData(obj2)
24: ∀ obj, app · (app ∈ dom(AppData) ∧ obj ∈ OS_Obj ∧ obj ∈ dom(ObjData) ∧ app ≠ ContainerOf(obj)) ⇒ ObjData(obj) ≠ AppData(app)
25: ∀ app, app1, app2 · (app ∈ dom(AppData) ∧ app2 ∈ dom(AppData) ∧ app1 ∈ NonTrusted_OS ∧ app = app1 ∧ app1 ≠ app2 ∧ AppData(app) = AppData(app2)) ⇒ ⊥

Во-вторых, в файле Machine я описываю:

prf_1:  ∀app1, app2 · ((action = read) ∧ app1 ∈ NonTrusted_OS ∧ app2 ∈ dom(AppData) 
∧ app1 ≠ app2 ∧ src = app1 ∧ dst = AppData(app2) 
∧ status ≠ initStt) ⇒ status = may_prevent 

prf_2: ∀app · ((action = read ∨ action = write) ∧ app ∈ dom(AppData) 
∧ src = app ∧ dst = AppData(app) ∧ status ≠ initStt) ⇒ status = shall_permit

И два события: два события
После этого событие-B генерирует обязательства по проверке и пытается доказать последовательность. Однако эти два требования противоречат друг другу: неисполненное обязательство по доказательству
В поле цели: он не может доказать, что:
A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))) правда.
Однако в требовании № 2 имеем: app1 ≠ app2
=> app ≠ app2 (because app1=app)=> AppData(app2) ≠ AppData(app)Следовательно, (app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app) = ЛОЖЬ
тогда A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))) = ИСТИНА.

Не могли бы вы дать мне несколько советов или комментарий, пожалуйста?

Answer 1

Я немного догадываюсь здесь, так как ваша модель довольно длинная, и не очевидно, что идет не так или что нужно доказать. Вы можете улучшить свой вопрос, удалив неиспользуемые вещи.

Вы хотите доказать

¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))

(Я не понимаю часть A=, правая часть - это предикат, а не выражение.)

Давайте применим различие в регистре app∈dom(AppData) ∧ app1=app:

• Если оно ложно, то весь предикат тривиально верен.

• Если это правда, у нас есть это как дополнительная гипотеза, и нам осталось доказать (*):

  ¬(AppData(app2)=AppData(app1))
  

На скриншоте видно, что app1 ≠ app2Таким образом, чтобы создать экземпляр аксиомы 22, вам все еще нужно app2∈dom(AppData) чтобы получить нужный результат AppData(app2)≠AppData(app1), Это не видно на вашем скриншоте, но может быть где-то там.

(*): Может быть, вы можете достичь этого, представив гипотезу ¬(AppData(app2)=AppData(app1)) ("ах"). После этого вы можете использовать это и гипотезу из вышеупомянутого различия, чтобы доказать свою цель.

Просто комментарий: аксиомы 22 и 23 могут быть полностью заменены путем определения функций AppData а также ObjData как инъективный, например ObjData ∈ OS_Obj -+>> DataSecs, Это не только сделало бы спецификацию более читабельной, я думаю, что проверяющие могут справиться с ними лучше, чем количественные утверждения.