事件 B 证明义务

Question

我在事件-B 中无法履行证明义务。在我的工作中，我想形式化内存保护要求的规范，以检查它们之间的一致性。为此，我使用 Event-B Context 来形式化系统的结构，并使用 Event-B Machine 来描述需求。每个要求都在不变量和事件中进行了描述。事件 B 将检查每对要求以找出不一致之处。
但是，它不能证明两个要求是一致的： 1: "Read 从 NonTrusted 到 的 data_section 的访问其他 OS_Apps 是 may_prevent"
2：“读取和写入 从 OS_App对其自己的data_section是shall_permit"

这是我的作品。首先，在上下文文件中，我描述了系统的结构和访问控制：
1。系统结构：
我们有 2 种类型的 OS_Application：Trusted 和 NonTrusted.
2 种 OS_Objects：Tasks 和 ISRs。
2 种 ISR：Category_1 和 Category_2。
每个OS_Object属于一个OS_App：ContainerOf∈OS_Obj→OS_App
每个OS_App都有一个代码段：AppCode∈OS_App→CodeSection
内存有两部分：DataSection 和 Stack
OS_App和OS_Obj可能有DataSection:

AppData ∈ OS_App ⇸ DataSecs
ObjData ∈ OS_Obj ⇸ DataSecs

OS_Obj有自己的Stack: ObjStack ∈ OS_Obj → Stacks

2。访问控制：
访问是从 Subjects 到 Objects:
主题包括：OS_App和OS_Obj
对象包括：Code_Section和内存
在下面的代码中，第 20 行 描述：“根据定义，这些对象的堆栈只属于所有者对象，因此不需要在对象之间共享堆栈数据，即使这些对象属于同一个 OS-Application。”

第 21 行 描述：“代码部分对于 OS-应用程序是私有的，或者可以在所有应用程序之间共享OS-应用程序”
第 22、23 行 描述：“OS-应用程序可以有私有数据部分，Tasks/ISRs 可以有私有数据部分”
第 24 行 描述：“OS-应用程序的私有数据部分由所有人共享 Tasks/ISRs 属于那个 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)) ⇒ ⊥

其次，在机器文件中，我描述：

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

还有两个事件：Two events
之后，事件 B 生成 Proof Obligations 并尝试证明一致性。但是，这两个要求不一致，如下所示： undischarged Proof Obligation
在目标框中：它不能证明：
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) = FALSE
那么 A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))) = TRUE.

你能给我一些提示或评论吗？

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))（通过"ah"）来实现这一点。之后你可以用这个和上面案例区分的假设来证明你的目标。

只是评论：公理 22 和 23 可以通过将函数 AppData 和 ObjData 定义为单射来完全替换，例如ObjData ∈ OS_Obj -+>> DataSecs。这不仅会使规范更具可读性，而且我认为证明者可以比量化陈述更好地处理这些问题。

事件 B 证明义务

Event-B Proof Obligations

operating-system

formalize

event-b