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

吕永阳 等: XCMP 协议的形式化验证与改进: 提升跨链交互安全性 2495

6.1.1 协议建模
在本节中, 首先进行模式定义, 随后基于模式定义进行操作定义, 实现对 E-XCMP 协议的系统性建模.
(1) 模式定义
(a) 消息模式
● Add: Parachain 消息的接收方.
● T: Z 消息的时间戳.
● N: N 消息所属区块中消息的个数, 用于确保消息在区块内的完整性.
● X: string 消息所属区块的唯一标识符.
● m: string 表示跨链数据的具体内容.
● size: Z 消息大小.
size ⩽ maxMessageSize 确保每条消息的大小在预定限制内, 以保证消息传递在资源限制范围内进行. 具
约束
体见代码 11.

代码 11. Message.
Add: Parachain
T: Z
N: N
X: string
m: string
size: Z
size ≤ maxMessageSize
(b) 区块模式
● Xi: string 表示该区块的唯一标识符, 用于标识每个区块.
● messages: seq Message 是一个消息序列, 表示该区块中包含的所有消息.
∀m : Message|m ∈ ran messages@m.X=Xi 确保区块中所有消息的标识符 m.X 与区块的标识符 Xi 一
约束条件
致. 这意味着每条消息都必须与所属区块匹配, 确保消息的正确关联和完整性. 具体见代码 12.
代码 12. Block.

Xi: string
message: seq Message

∀ m: Message | m ∈ ran messages · m.X=Xi
(c) 平行链状态模式
● ingressQueue: seq Message 平行链的入口队列.
● egressQueue: seq Message 平行链的出口队列.
● dot: DOT 表示平行链的存储资源, 用于管理通道的存款和交易费用.
约束条件 ∀m : Message|m ∈ ran ingressQueue∨m ∈ ran egressQueue@m.size ⩽ maxMessageSize 确保所有消息, 无
论是在入口队列还是出口队列中, 其大小都不超过最大消息大小 maxMessageSize. 具体见代码 13.

代码 13. ParachainState.
ingressQueue: seq Message