资料下载
×
高安全性应用开发环境的时序性质验证框架
消耗积分:0 |
格式:pdf |
大小:2.04 MB |
2021-05-28
分享资料个
高安全性应用开发环境（ SCADE）的形式化验证组件 Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质，但不能充分描述拥有复杂时序性质的安全需求。为解决该问题，构建一种 SCADE状态机的时序性质验证框架，将 SCADE模型转换成№usSMⅤ模型，并将线性时态逻辑和计算树逻辑引入 SCADE模型的需求规范中。分析结果表明，借助 Nusmv模型检查器及其验证结果可检验复杂时序相关的安全性质，减少模型设计阶段的错误，提高系统的安全性和可靠性。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
