资料下载
×
时序逻辑符号模型检测器
消耗积分:2 |
格式:rar |
大小:1.13 MB |
2018-01-26
分享资料个
现有模型检测工具的形式化规范语言。如计算树逻辑（computation tree logic，简称CTL）和线性时序逻辑（Linear temporal logic，简称LTL）等的描述能力不足，无法验证∞正则性质．提出了一个命题投影时序逻辑（propositional proj ection temporal logic，简称PPTL）符号模型检测工具-PLSMC（PPTL symbolic model checker）的设计与实现过程．该工具基于著名的符号模型检测系统NuSMV，实现了PPTL的符号模型检测算法．PLSMC的规范语言PPTL具有完全正则表达能力，这使得定性性质和定量性质均可被验证．此外，PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题，最后，利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证，实验结果表明，PPTL符号模型检测工具扩充了NuSMV系统的验证能力，使得时间敏感、并发性和周期性等实时性质可以被描述和验证．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
