目录

1. Specification Process

1.1 State Invariants

1.2 Exceptional Behaviour

1.3 Framing

1.4 Summary

2. V&V FOR SPECS

2.1 V&V for formal specs

2.2 Proof

2.3 Proof Assistants

2.4 Model Checking

---

1. Specification Process

Specification Process关注如何编写用于描述系统状态的断言和谓词。

1.1 State Invariants

这部分主要解释了状态机（State Machine）和状态断言的概念。这里的状态（State）指的是系统在给定时间点的状态。每一个操作都可能导致系统状态的改变。我们通常用一种称为断言（assertion）的方式来验证状态的性质。

例如，一个状态机可以用如下的方式进行描述：S0 (Init) --Opi-> S1 --Opj-> S2 ... --Opk-> Sn，其中S0, S1, S2...Sn代表不同的状态，Opi, Opj, Opk等代表可能的操作。

其中的Inv[s]是一个谓词（predicate），它用于描述系统状态s是否满足某种性质。验证Inv[s]是否对所有状态s都成立，可以通过以下两个断言：

assert invInit { all s : State | Init[s] => Inv[s] }
assert invOpi { always all s : State | Inv[s] and Opi[s] => after Inv[s] }

其中invInit确保所有初始状态都满足Inv[s]，invOpi确保在执行操作Opi后，新的状态依然满足Inv[s]。这里的"always"和"after"关键词分别表示所有状态和操作后的状态。

1.2 Exceptional Behaviour

Distinguishing normal and exceptional behaviour in models

//Add a password for a *new* user/url pair
pred addNormal [pb : PassBook, url : URL, user : Username, 
			   pwd: Password, report : one Report] {
	addPre [pb, url, user]
	addPost [pb, url, user, pwd]
	report in Success
}

//Fail to add a password that already exists
pred addExceptional [pb : PassBook, url : URL, user : Username,
				report : one Report] {
	not addPre [pb, url, user]
	pb.password' = pb.password
	report in Failed
}

//Add a password for a *new* user/ url, otherwise, add nothing 
pred add [pb : PassBook, url : URL, user: Username, pwd: Password,
		report :one Report]s
	addNormal [pb, url, user, pwd, report]
	 or
	addExceptional [pb, url, user, report]
}

The point is to constrain what the system is meant to do in exceptional cases

//Fail to add a password that already exists
pred addExceptional [pb : PassBook, url : URL, user : Username,
				report : one Report] {
	not addPre [pb, url, user]
	pb.password' = pb.password
	report in Failed
}

Model it separately from normal behaviour
Where does it come from?
e.g. Hazard Analysis (HAZOP) etc

这部分讲述了正常和异常行为的区分以及如何在模型中描述这两种行为。

对于每个操作，我们都需要描述其正常情况下的预期行为以及异常情况下的行为。例如，在以下的密码添加示例中，addNormal定义了正常情况下的预期行为，而addExceptional定义了异常情况下的行为。

异常行为的来源可以通过危害分析（Hazard Analysis，如HAZOP）等方法进行识别。

1.3 Framing

这部分主要讨论了命题（predicate）的范围问题。

例如，在以下两个addExceptional的定义中，第二个版本去掉了pb.password' = pb.password这一句，因此在后续状态中，pb.password的值可以是任何值，这使得异常行为可以是任意的。

How are these two predicates different?

//Fail to add a password that already exists
pred addExceptional [pb : PassBook, url : URL, user : Username,
				report : one Report] {
	not addPre [pb, url, user]
	pb.password' = pb.password
	report in Failed
}


//Fail to add a password that already exists
pred addExceptional [pb : PassBook, url : URL, user : Username,
				report : one Report] {
	not addPre [pb, url, user]
	//pb.password' = pb.password
	report in Failed
}

Second allows pb.password in the post-state to be anything, and so allows add’s exceptional behaviour to be arbitrary

What does this spec say?

Imagine that Objs have two variable fields, x and y

Allows the y field to change arbitrarily. It should be:

另外一个例子展示了如何通过限制字段的变化来约束系统的行为。例如，addToX的第一个版本只限制了x字段的变化，而y字段可以随意变化。然而在第二个版本中，我们增加了o.y’ = o.y以确保y字段在执行addToX操作时保持不变。

1.4 Summary

• State: 在理解状态机的时候，重要的是要知道状态和转换。状态表示系统的某一特定情况，而转换则表示从一个状态到另一个状态的动作或条件。在软件工程中，状态机经常用于建模系统的行为。

• Exceptional Behaviour: 异常行为通常指系统的非正常或错误行为。在设计系统时，特别是关键系统（如医疗或航空系统），处理异常行为是非常重要的。如果未能妥善处理，异常行为可能会导致系统故障或更严重的后果。

• Framing: Framing是指在进行操作时，明确指定哪些变量或属性应该发生变化，哪些应该保持不变。这是一个重要的概念，因为如果不进行framing，系统的行为可能会超出预期。在某些情况下，我们希望某些属性在执行操作时保持不变，这就需要使用framing来明确指定。

2. V&V FOR SPECS

2.1 V&V for formal specs

V&V代表验证与确认，是一个对系统或产品进行评估，确保其满足特定需求、功能和性能的过程。在我们的规格中，我们使用各种方法进行V&V，包括动画、模型检查、实现与测试、审查与检查、以及证明。

1. Animation & Model Checking (以Alloy为例)

• 动画（如Alloy的run命令）：Alloy是一个轻量级的形式方法工具，能用于创建和分析模型。动画就是通过命令将模型实例化并进行模拟，让开发者可以看到模型的运行情况，对模型进行验证。

• 模型检查（如Alloy的check命令）：模型检查是一种自动化的技术，可以全面地检查一个系统的所有可能状态是否满足某个特性。在Alloy中，check命令用于验证一个模型是否满足一个或多个断言。

2.2 Proof

• 证明是一个重要的V&V方法。幻灯片中的例子展示了如何使用证明来验证add操作。这个操作有两种情况，addNormal和addExceptional，对应着添加密码的正常和异常情况。

• 对每一种情况，都需要证明在执行add操作后，系统的状态依然满足某种属性（即Inv[pb]）。这个证明过程被分解成了几个步骤，包括原始情况（Case 1）和变化情况（Case 2）。

• 幻灯片中使用的是一种称为Hoare逻辑的方法，其中的assert语句形式为{P}C{Q}，其中P是程序C执行前的条件，Q是程序C执行后的条件。这种方法用于证明在满足某些条件的情况下，程序的执行会导致另一些条件的满足。

add[pb, user, url, pwd, res] =
    addNormal[pb, user, url, pwd, res] or
    addExceptional[pb, user, url, res]

在这里，我们有一个add函数，这个函数接收五个参数：pb（密码本），user（用户），url（地址），pwd（密码）和res（结果）。这个函数定义为addNormal和addExceptional两个函数的并集。也就是说，add函数要么按照正常情况添加密码（即addNormal），要么按照异常情况添加密码（即addExceptional）。

Invariants and Operation

all pb, user, url, pwd, res |
Inv[pb] and add[pb,user,url,pwd,res] =>
after Inv[pb]

这是一个表达式，表示的是对于所有的密码本（pb），用户（user），地址（url），密码（pwd）和结果（res）的组合，如果满足初始状态Inv[pb]并且执行了add操作，那么就会满足结束状态after Inv[pb]。这就是形式化验证中常见的前置条件和后置条件的写法。

在这一部分，我们看到两种添加密码的情况，addNormal和addExceptional。我们要对这两种情况进行分别考虑。

在Case 1中，我们看到addNormal函数的定义和行为。

Case 1
addNormal[pb, user, url pwd, res] =
 no pb.password[user][url]
 pb.password’ = pb.password + (user->url->pwd)
 res in Success

all pb, user, url, pwd, res |
 Inv[pb] and addNormal[pb, user, url, pwd, res]) =>
after Inv[pb]

这表明，在正常添加情况下，首先确认密码本中没有该用户在此地址的密码（no pb.password[user][url]）。然后，我们将新的密码添加到密码本中（pb.password’ = pb.password + (user->url->pwd)），并返回成功结果。

随后，我们有一系列的表达式，来证明如果在满足初始状态Inv[pb]并执行了addNormal操作后，我们依然满足after Inv[pb]。

Case 1

addNormal[pb, user, url pwd, res] =
 no pb.password[user][url]
 pb.password’ = pb.password + (user->url->pwd)
 res in Success

all pb, user, url, pwd, res |
 Inv[pb] and no pb.password[user][url] and
 pb.password’ = pb.password + (user->url->pwd) =>
after Inv[pb]

Case 1

Inv[pb] = all user, url | lone pb.password[user][url]

all pb, user, url, pwd, res |
 Inv[pb] and no pb.password[user][url] and
 pb.password’ = pb.password + (user->url->pwd) =>
after Inv[pb]

Case 1

Two cases to consider: user2, url2 are user, url or not

all pb, user, url, pwd, res |
 (all user1, url1 | lone pb.password[user1][url1]) and
 no pb.password[user][url] and
 pb.password’ = pb.password + (user->url->pwd) =>
(all user2, url2 | lone pb.password’[user2][url2])

在Case 1.1和Case 1.2中，我们进一步考虑了用户和地址是否在密码本中的两种情况。

Case 1.1

user2, url2 are user, url

all pb, user, url, pwd, res |
 (all user1, url1 | lone pb.password[user1][url1]) and
 no pb.password[user][url] and
 pb.password’ = pb.password + (user->url->pwd) =>
(lone pb.password’[user][url])

Case 1.2

user2, url2 are not user, url

all pb, user, url, pwd, res |
 (all user1, url1 | lone pb.password[user1][url1]) and
 no pb.password[user][url] and
 pb.password’ = pb.password + (user->url->pwd) =>
(all user2, url2 | lone pb.password’[user2][url2])

在Case 2中，我们看到了一个与Case 1类似的情况，但这次是对addExceptional函数的处理。也就是说，在异常情况下，我们也要保证如果在满足初始状态Inv[pb]并执行了addExceptional操作后，我们依然满足after Inv[pb]。

Case 2

Similar.

all pb, user, url, pwd, res |
 Inv[pb] and addExceptional[pb, user, url, pwd, res]) =>
after Inv[pb]

2.3 Proof Assistants

• 证明助手是一种工具，可以帮助自动化证明过程。例如，Isabelle，Coq，HOL4等是一些著名的定理证明工具，它们可以帮助程序员更高效地完成证明任务。

• 另外，还有一些自动化的证明工具，如SAT和SMT求解器，例如MiniSAT和Z3。这些工具可以自动地找到满足某些条件的解，或者证明这样的解不存在。

2.4 Model Checking

• 模型检查是另一种V&V方法，用于自动检查系统的所有状态是否满足某种属性。当检查失败时，模型检查工具可以给出一个反例，即一个使得属性不成立的状态。

• 模型检查在硬件验证和安全协议验证等领域有很多成功的应用。