事件B证明义务

Question

我在事件B中有问题来履行证明义务。在我的工作中，我想正式确定内存保护要求的规范，以检查它们之间的一致性。为了做到这一点，我使用了Event-B上下文来形式化系统结构，并使用Event-B Machine来描述需求。 Invariant和Event都描述了每个需求。事件-B将检查每对要求以找出不一致。
但是，它不能证明两者的要求是一致的： 1： “从读访问不可信到DATA_SECTION其他OS_Apps是may_prevent”
2：“读取和写入从OS_App其自己DATA_SECTION访问是shall_permit“

这是我的工作。首先，在上下文文件中，我描述了系统的结构和访问控制：
1.系统的结构：
我们有2种OS_Application的：可信和不可信。
2种类型的OS_Objects：任务和ISR。
2种ISR：Category_1和Category_2。
每个OS_Object属于一个OS_App：ContainerOf∈OS_Obj→OS_App
每个OS_App具有代码部分：AppCode∈OS_App→CodeSection
存储器具有两个部分：DataSection和堆栈
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，和内存
在下面的代码，线20描述道：“堆叠这些对象，根据定义，只属于所有者对象，因此没有必要共享对象之间的堆栈数据，即使这些对象属于相同的OS应用程序“。

线21描述： “代码部分为私人到OS的应用程序或可以全部OS的应用程序之间共享” 线22
，23描述：“OS的应用程序可以有私人数据部分，任务/ ISR可以有私人数据部分。“
线24描述：“OS的应用程序的专用数据部分是由属于该OS-应用所有任务/ ISR的共享”

通过分析，我定义上下文如下：

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生成证明义务，并试图证明的一致性。但是，这两个要求不一致如下： undischarged Proof Obligation
在目标框中：它不能证明：
A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)))为真。
然而，在要求二号，我们有：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。这不仅会使规范更具可读性，我认为证明者可以处理那些比量化语句更好的东西。