嵌入式系统数据缓存机制的形式化分析

摘要

嵌入式系统在高速通信时通常需要设计缓存机制以保证数据不会丢失,以某嵌入式系统为例,介绍了该系统的硬件及软件平台的设计,利用模型检查工具SPIN对该系统的数据缓存机制进行形式化建模,并利用时态逻辑公式LTL描述了该系统待验证属性,验证结果表明,该缓存机制满足设计需求,为嵌入式系统数据交互设计提供了严密的研究论证方法.