论文部分内容阅读
模型检验作为一种形式化验证方法，近年来在各种硬件、软件设计中得到了广泛应用．文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑，然后介绍了模型检验中常用的两种算法：标记算法和基于固定点的算法，最后介绍了为避免内存爆炸而引入的符号模型检验技术．
一种形式化验证方法：模型检验
【摘 要】
：
模型检验作为一种形式化验证方法，近年来在各种硬件、软件设计中得到了广泛应用．文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑，然后介绍了模型检验中常用的
【机 构】
：
浙江大学超大规模集成电路设计研究所
【出 处】
：
浙江大学学报：理学版
【发表日期】
：
2006年4期
【基金项目】
：
国家自然科学基金资助项目（No.90207002）.
其他文献
通过对汶川8.0级地震的类型和破裂特征分析,讨论了龙门山构造带地震活动与甘肃省地震活动的关系。回顾了对汶川地震序列的动态跟踪过程以及余震活动在甘肃省的震情判定过程。
相互作用herding模型定性上能很好地呈现一些真实的经济规律，但定量上与真实的市场还有一定的距离，特别是收益绝对值的自关联衰退得太快．通过数值模拟研究发现该模型在它的参数
研究极限跟踪性与伪轨跟踪性的关系及极限跟踪性的某些性质,证明了紧致度量空间上有POTP的等度连续自同胚有极限跟踪性;若紧致度量空间上的自同胚f有极限跟踪性,则其链回归集