资料下载
×
基于模拟关系的时间自动机精化检测方法
消耗积分:2 |
格式:rar |
大小:1.44 MB |
2018-01-16
分享资料个
精化检测是一种重要的形式化验证方法，将系统实现和性质规约用相同的形式化语言进行建模，如能证明两者间存在某种精化关系，且该关系能够维持性质，可得出系统实现满足性质规约，为验证不同类型的系统性质，traces，stable failures和failures-divergence精化检测方法已被提出．精化检测算法依赖于子集构造，因而其面临状态空间爆炸问题，近年来，已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法，极大地提高了算法的性能，且该方法能够直接用于traces精化检测．在此基础上，提出了基于模拟关系的stable failures和failures-divergence精化检测方法，此外，还将精化检测扩展到了时间系统的验证中，提出了基于模拟关系的时间自动机traces精化检测方法，实验结果表明，基于模拟关系的算法效率有很大提高．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
