一种基于模型转换的状态机模型时序性质验证系统专利查询专利号|摘要-满商公司网

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

基本信息

申请号	CN201910605386.1	申请日	-
公开（公告）号	CN110532166A	公开（公告）日	2019-12-03
申请公布号	CN110532166A	申请公布日	2019-12-03
分类号	G06F11/36	分类	计算；推算；计数;
发明人	黄滟鸿;史建琦;张继;郭欣;施健	申请（专利权）人	上海丰蕾信息科技有限公司
代理机构	北京辰权知识产权代理有限公司	代理人	刘广达
地址	200062 上海市普陀区中山北路3663号
法律状态	-

摘要

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