Moore机表示的系统迭代设计动态CTL模型检验的不变性研究(英文)

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

On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System

Model checking is a promising approach to verifying safety properties of trusted computing systems in the design phase of system-level.Dynamic model checking is the model checking in which the model changes frequently along the design process.A serious problem for dynamic model checking is that the cost of re-checking is too expensive due to model being changed trivially,so a key issue of the problem is to seek invariance in order to avoid the checking repeatedly.An invariance is a true predicate that will ...