科研之友
微信
新浪微博
Facebook
分享链接
摘要
本申请公开了一种基于模型转换的状态机模型时序性质验证系统,包括：模型解析模块,用于解析SCADE文本模型,得到语法树实例；符号表容器模块,用于装载语法树实例,得到符号表实例；模型转换模块,用于根据模型转换规则将符号表实例转换为NuSMV模型；模型检查模块,用于根据LTL公式及CTL公式验证NuSMV模型的时序性质。通过解析高安全性的应用程序开发环境SCADE文本模型,将SCADE文本模型转换为NuSMV模型,根据LTL公式及CTL公式验证NuSMV模型的时序性质,从而实现验证SCADE文本模型的时序性质,突破了SCADE模型性质验证的这个限制,进一步提高软件系统的安全性与可靠性。通过为SCADE形式化验证引入能够描述时序相关安全需求的时序规范,从而能够验证模型的时序性质。
- 单位
