论文部分内容阅读
模型检验是系统级设计中验证可信计算系统安全性性质的有效方法。动态模型检验是模型随设计过程而变化的模型检验，动态模型检验过程中遇到的最严重问题之一是模型变化所带来的重复检验代价太高。因此，寻找不变性以避免重复检验显得尤为重要。不变性是一种贯穿系列模型检验而保值为真的性质。该文构建动态模型检验的形式化框架，进而提出基于Moore机描述的流控制系统迭代设计过程的不变性理论，该系统是一种嵌入式控制系统，在可信通信中用以处理数据转换，最后展示了若干非平凡CTL性质在迭代过程中的可保持性。