×

高安全性应用开发环境的时序性质验证框架

消耗积分:0 | 格式:pdf | 大小:2.04 MB | 2021-05-28

分享资料个

　　高安全性应用开发环境（ SCADE）的形式化验证组件 Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质，但不能充分描述拥有复杂时序性质的安全需求。为解决该问题，构建一种 SCADE状态机的时序性质验证框架，将 SCADE模型转换成№usSMⅤ模型，并将线性时态逻辑和计算树逻辑引入 SCADE模型的需求规范中。分析结果表明，借助 Nusmv模型检查器及其验证结果可检验复杂时序相关的安全性质，减少模型设计阶段的错误，提高系统的安全性和可靠性。

下载并关注上传者 开通VIP，低至0.08元下载/次

声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉

评论(0)
发评论

下载排行榜

全部0条评论

快来发表一下你的评论吧 !