Page 181 - 《软件学报》2026年第6期

2500 软件学报 2026 年第 37 卷第 6 期

(返回值为 1), 即资产转移操作成功. 如果验证失败, 则删除块标识 Xi?相关的消息 (DeleteMessage Xi?=1), 并扣除
过错方的 DOT 代币 (deductDot(S, D)=1).

代码 19. PromiseValidate.
ΞFishman
Xi?: string
N?: N
S, D: Parachain
ΔRelaychainState
N
DBlockPMN: string→
DBlockcont: string→ N
newBlock: Block
DBlockcont Xi?=N?

Xi? ∈ dom fishmaxPMN
if DBlockPMN Xi?=fishmanPMN Xi?
then newBlock=mkBlockXi? ∧ AssetTransfer newBlock =1
else DeleteMessage Xi?=1 ∧ deductDot(S, D)=1 ∧ ¬Xi? ∈ validatedXi
(d) 区块验证模式 (ValidateBlock)
在 ValidateBlock 操作中, 区块验证的流程如图 11 所示, 详细代码如代码 20 所示. 主要目标是验证新块 newBlock
并更新中继链状态, 主要步骤如下.

Collator D
① 将新生成的区块提交 ② 当确认无误后, 将区块
给Validator D 进行验证 添加到中继链的尾部,
跨链操作得到确认
平行链D Validator D 中继链
图 11 区块验证流程图

① 首先, 将新生成的区块交给 Validator D , 通过 validateBlock 函数对新块 newBlock?进行验证. 如果验证成功,
validateBlock newBlock?的结果为 1.
② 若验证成功, 则将新块 newBlock?添加到中继链的已验证区块序列 validatedBlock 中. 同时, 将新块的块标
识 Xi 添加到已验证块标识的集合 validatedXi 中, 形成新的 validatedXi'.
代码 20. ValidateBlock.

ΔRelaychainState
newBlock?: Block
validateBlock newBlock?=1
∧ 〈newBlock?〉
⇒ validateBlock'=validatedBlock
∧ validatedXi'=validatedXi ∪ {newBlock?.Xi}
6.1.2 形式化验证
在此建模的基础上, 本节使用 Z/EVES 工具对 E-XCMP 协议进行形式化验证. 通过构建 3 个定理, 对应协议
的 3 条安全目标, 利用 Z/EVES 的自动化定理证明功能, 严格验证了这些目标的符合性, 确保每条安全目标都在形
式化模型中得到充分证明.