-
公开(公告)号:CN110532167A
公开(公告)日:2019-12-03
申请号:CN201910606311.5
申请日:2019-07-05
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F11/36
Abstract: 本申请公开了一种基于模型转换的状态机模型时序性质验证方法,包括:模型解析步骤,解析SCADE文本模型,得到语法树实例;符号表容器步骤,装载语法树实例,得到符号表实例;模型转换步骤,根据模型转换规则将符号表实例转换为NuSMV模型;模型检查步骤,根据LTL公式及CTL公式验证NuSMV模型的时序性质。通过解析高安全性的应用程序开发环境SCADE文本模型,将SCADE文本模型转换为NuSMV模型,根据LTL公式及CTL公式验证NuSMV模型的时序性质,从而实现验证SCADE文本模型的时序性质,突破了SCADE模型性质验证的这个限制,进一步提高软件系统的安全性与可靠性。通过为SCADE形式化验证引入能够描述时序相关安全需求的时序规范,从而能够验证模型的时序性质。
-
公开(公告)号:CN110532167B
公开(公告)日:2021-05-04
申请号:CN201910606311.5
申请日:2019-07-05
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F11/36
Abstract: 本申请公开了一种基于模型转换的状态机模型时序性质验证方法,包括:模型解析步骤,解析SCADE文本模型,得到语法树实例;符号表容器步骤,装载语法树实例,得到符号表实例;模型转换步骤,根据模型转换规则将符号表实例转换为NuSMV模型;模型检查步骤,根据LTL公式及CTL公式验证NuSMV模型的时序性质。通过解析高安全性的应用程序开发环境SCADE文本模型,将SCADE文本模型转换为NuSMV模型,根据LTL公式及CTL公式验证NuSMV模型的时序性质,从而实现验证SCADE文本模型的时序性质,突破了SCADE模型性质验证的这个限制,进一步提高软件系统的安全性与可靠性。通过为SCADE形式化验证引入能够描述时序相关安全需求的时序规范,从而能够验证模型的时序性质。
-
公开(公告)号:CN110532166B
公开(公告)日:2021-05-04
申请号:CN201910605386.1
申请日:2019-07-05
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F11/36
Abstract: 本申请公开了一种基于模型转换的状态机模型时序性质验证系统,包括:模型解析模块,用于解析SCADE文本模型,得到语法树实例;符号表容器模块,用于装载语法树实例,得到符号表实例;模型转换模块,用于根据模型转换规则将符号表实例转换为NuSMV模型;模型检查模块,用于根据LTL公式及CTL公式验证NuSMV模型的时序性质。通过解析高安全性的应用程序开发环境SCADE文本模型,将SCADE文本模型转换为NuSMV模型,根据LTL公式及CTL公式验证NuSMV模型的时序性质,从而实现验证SCADE文本模型的时序性质,突破了SCADE模型性质验证的这个限制,进一步提高软件系统的安全性与可靠性。通过为SCADE形式化验证引入能够描述时序相关安全需求的时序规范,从而能够验证模型的时序性质。
-
公开(公告)号:CN110532166A
公开(公告)日:2019-12-03
申请号:CN201910605386.1
申请日:2019-07-05
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F11/36
Abstract: 本申请公开了一种基于模型转换的状态机模型时序性质验证系统,包括:模型解析模块,用于解析SCADE文本模型,得到语法树实例;符号表容器模块,用于装载语法树实例,得到符号表实例;模型转换模块,用于根据模型转换规则将符号表实例转换为NuSMV模型;模型检查模块,用于根据LTL公式及CTL公式验证NuSMV模型的时序性质。通过解析高安全性的应用程序开发环境SCADE文本模型,将SCADE文本模型转换为NuSMV模型,根据LTL公式及CTL公式验证NuSMV模型的时序性质,从而实现验证SCADE文本模型的时序性质,突破了SCADE模型性质验证的这个限制,进一步提高软件系统的安全性与可靠性。通过为SCADE形式化验证引入能够描述时序相关安全需求的时序规范,从而能够验证模型的时序性质。
-
公开(公告)号:CN106598590A
公开(公告)日:2017-04-26
申请号:CN201611137729.9
申请日:2016-12-12
Applicant: 华东师范大学
IPC: G06F9/44
CPC classification number: G06F8/20
Abstract: 本发明公开一种软件体系结构建模和仿真方法,包括:将输入的软件需求输出为层次化MAS软件模型,该模型作为仿真模块的输入;对输入的层次化MAS软件模型进行仿真,从而展示各个agent之间的交互行为。本发明公开的基于层次化MAS的软件体系结构建模与仿真方法在传统多agent软件体系上新增了层次化的设计模式,以功能为目标将软件功能与外部环境模块于统一架构内,完成了集分布式与集中式控制于一体的可应对动态环境变化的多层次MAS的自适应软件体系结构。
-
公开(公告)号:CN106598590B
公开(公告)日:2020-10-02
申请号:CN201611137729.9
申请日:2016-12-12
Applicant: 华东师范大学
IPC: G06F8/20
Abstract: 本发明公开一种软件体系结构建模和仿真方法,包括:将输入的软件需求输出为层次化MAS软件模型,该模型作为仿真模块的输入;对输入的层次化MAS软件模型进行仿真,从而展示各个agent之间的交互行为。本发明公开的基于层次化MAS的软件体系结构建模与仿真方法在传统多agent软件体系上新增了层次化的设计模式,以功能为目标将软件功能与外部环境模块于统一架构内,完成了集分布式与集中式控制于一体的可应对动态环境变化的多层次MAS的自适应软件体系结构。
-
公开(公告)号:CN106648833B
公开(公告)日:2020-10-02
申请号:CN201611137739.2
申请日:2016-12-12
Applicant: 华东师范大学
IPC: G06F9/455
Abstract: 本发明公开一种软件体系结构建模和仿真系统,包括:建模模块,用于将输入的软件需求输出为层次化MAS软件模型,该模型作为仿真模块的输入;仿真模块,用于对输入的层次化MAS软件模型进行仿真,从而展示各个agent之间的交互行为。本发明公开的基于层次化MAS的软件体系结构建模与仿真系统在传统多agent软件体系上新增了层次化的设计模式,以功能为目标将软件功能与外部环境模块于统一架构内,完成了集分布式与集中式控制于一体的可应对动态环境变化的多层次MAS的自适应软件体系结构。
-
公开(公告)号:CN106648833A
公开(公告)日:2017-05-10
申请号:CN201611137739.2
申请日:2016-12-12
Applicant: 华东师范大学
IPC: G06F9/455
Abstract: 本发明公开一种软件体系结构建模和仿真系统,包括:建模模块,用于将输入的软件需求输出为层次化MAS软件模型,该模型作为仿真模块的输入;仿真模块,用于对输入的层次化MAS软件模型进行仿真,从而展示各个agent之间的交互行为。本发明公开的基于层次化MAS的软件体系结构建模与仿真系统在传统多agent软件体系上新增了层次化的设计模式,以功能为目标将软件功能与外部环境模块于统一架构内,完成了集分布式与集中式控制于一体的可应对动态环境变化的多层次MAS的自适应软件体系结构。
-
-
-
-
-
-
-