资料下载
×
可检测实时系统的正确性的符号化模型
消耗积分:0 |
格式:rar |
大小:2.39 MB |
2021-05-07
分享资料个
实时系统的错误往往十分危险甚至是致命的，使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题，文中首先提岀一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑（ Real-time linearυ ynamic logic， RTLDL）;然后使用类似程序控制流标记的方法为 RTLDI·公式定义起止标记，根据起止标记关系构造时态测试器，提出基于时态测试器的 RTLDI符号化模型检测算法;最后基于翻译的方法在模型检测器NuⅩmν上实现了所提算法，并针对护栏控制系统案例与线性动态逻辑（ Inearυyaπ ic logic，LDL）模型检测器MCMASLDLK进行实验比较。实验结果表明，无论对于IDL还是 RTLDI公式的检测，提出的算法的效率均显著优于MCMAS-LDLK。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
