一种基于模型转换的状态机模型时序性质验证方法

摘要

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