1

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

这是我的工作。首先，在上下文文件中，我描述了系统的结构和访问控制：
1. 系统的结构：
我们有两种类型的 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
内存有 2 个部分：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：
Subjects包括：OS_App和OS_Obj
Objects包括：Code_Section和Memory
在下面的代码中，第20行描述：“这些对象的堆栈，根据定义，只属于所有者对象，因此不需要在对象之间共享堆栈数据，即使这些对象属于同一个操作系统应用程序。”

第 21 行描述：“代码部分是 OS 应用程序私有的，或者可以在所有 OS 应用程序之间共享”
第 22、23 行描述：“OS 应用程序可以有私有数据部分，而任务/ISR 可以有私有数据部分。 "
第 24 行描述：“操作系统应用程序的私有数据部分属于该操作系统应用程序的所有任务/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

以及两个事件：两个事件
之后，事件-B 生成 Proof Obligations 并尝试证明一致性。但是，这两个要求是不一致的，如下： undischarged Proof Obligation
In the Goal box：它不能证明：
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。

请给我一些提示或评论好吗？

4

1 回答 1

0

我在这里有点猜测，因为您给定的模型很长，而且不明显出了什么问题或应该证明什么。您可以通过删除未使用的东西来改善您的问题。

你想证明

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

（部分看不懂A=，右边是谓词，不是表达式。）

让我们在 上应用案例区分app∈dom(AppData) ∧ app1=app：

  • 如果它是假的，那么整个谓词就是微不足道的。

  • 如果它是真的，我们把它作为一个额外的假设，它还有待证明 (*)：

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

从您的屏幕截图中，我们可以看到app1 ≠ app2，因此要实例化 axiom 22，您仍然需要app2∈dom(AppData)获得所需的结果AppData(app2)≠AppData(app1)。它在您的屏幕截图中不可见，但可能在某处。

(*)：也许你可以通过引入一个假设来实现这一点¬(AppData(app2)=AppData(app1))（通过“啊”）。之后，您可以使用此和上述案例区分中的假设来证明您的目标。

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

于 2017-07-19T11:21:23.443 回答