买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉南京航空航天大学申请的专利一种基于大模型的安全关键软件验证性质自动生成方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN119473842B 。

龙图腾网通过国家知识产权局官网在2026-01-06发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202411348471.1，技术领域涉及：G06F11/3604；该发明授权一种基于大模型的安全关键软件验证性质自动生成方法是由杨志斌;周敏;周勇;王喜龙;王翰丰设计研发完成，并于2024-09-26向国家知识产权局提交的专利申请。

本一种基于大模型的安全关键软件验证性质自动生成方法在说明书摘要公布了：本发明公开了一种基于大模型的安全关键软件验证性质自动生成方法，包括：从各原子命题中提取出其中的主语和谓语，对提取出的主语和谓语进行合并，得到重组后的原子命题；定义不规范自然语言类型模板；按照定义的不规范自然语言类型模板，利用随机算法，将重组后的原子命题与逻辑算子进行结合，生成信号时序逻辑公式；并利用大语言模型，将其翻译为自然语言，从而构建得到包含公式‑自然语言对的数据集；根据情况选择使用包含公式‑自然语言对的数据集微调本地大模型或大语言模型接口，得到微调后的大模型；利用提示词模板，将待需要翻译的自然语言需求输入至微调后的大模型中，得到对应的时序逻辑公式。

本发明授权一种基于大模型的安全关键软件验证性质自动生成方法在权利要求书中公布了：1.一种基于大模型的安全关键软件验证性质自动生成方法，其特征在于：包括以下步骤： 对安全关键软件开发过程中的需求文本进行分析，得到需求文本中的原子命题，从各原子命题中提取出其中的主语和谓语，对提取出的主语和谓语进行合并，得到重组后的原子命题； 对安全关键软件开发过程中的需求文本进行分析，定义不规范自然语言类型模板； 按照定义的不规范自然语言类型模板，利用随机算法，将重组后的原子命题与逻辑算子进行结合，生成信号时序逻辑公式； 将生成的信号时序逻辑公式翻译为自然语言，从而构建得到包含公式-自然语言对的数据集； 根据情况选择使用包含公式-自然语言对的数据集微调本地大模型或大语言模型接口，得到微调后的大模型； 利用提示词模板，将待需要翻译的自然语言需求输入至微调后的大模型中，得到对应的时序逻辑公式； 所述不规范自然语言类型模板包括： 模板一： 当自然语言中含有：subjectverb_1operatorverb_2，将其补全为：subjectverb_1operatorsubjectverb_2；其中，subject表示主语，verb_1表示谓语1，operator表示and或imply或equal或or或until或until[*,**]； 当自然语言中含有：subjectoperatorsubjectverb，将其补全为：subject_1verboperatorsubject_2verb；其中，operator表示and或or； 模板二： 当自然语言中含有phrase+subject_1subject_2…+verb，将其补全为：subject_1verbandorsubject_2verbandor…；其中，phrase表示allof或oneof或anyof； 模板三： 当自然语言句式为：AP_1equalAP_2.AP_2+sentence，将其改写为：AP_1+sentence；其中，AP_1表示原子命题1，AP_2表示原子命题2； 模板四： 当自然语言句式为：APimplysentence_1,phraseimplysentence_2时，将其补全为APimplysentence_1和negationAPimplysentence_2两句；其中，AP表示原子命题，phrase为otherwise或ontheotherhand或conversely，sentence_1表示STL子公式1，sentence_2表示STL子公式2； 所述的按照定义的不规范自然语言类型模板，利用随机算法，将重组后的原子命题与逻辑算子进行结合，生成信号时序逻辑公式，具体包括： 定义一元运算符和二元运算符，所述一元运算符包括：否定、全局、最终，所述二元运算符包括：与、或、直到、蕴含、等价； 通过二叉树生成算法，将重组后的原子命题与适当的一元运算符和二元运算符随机合成，得到各种信号时序逻辑公式； 所述的通过二叉树生成算法，将重组后的原子命题与适当的一元运算符和二元运算符随机合成，得到各种信号时序逻辑公式，具体包括： 定义随机生成原子命题数AP_num和不规范类型irrgular_type； 随机选取AP_num个重组后的原子命题组成prop_list； 在irregular_type=1时在prop_list中插入一个type1_phrase，形成新的prop_list，基于新的prop_list，利用generate_from_list算法生成中序信号时序逻辑公式，得到最终的信号时序逻辑公式，表示为：generate_from_listprop_list； 在irregular_type=2时在prop_list中插入一个type2_phrase，形成新的prop_list，基于新的prop_list，利用generate_from_list算法生成中序信号时序逻辑公式，得到最终的信号时序逻辑公式，表示为：generate_from_listprop_list； 在irregular_type=3时，随机取样一个重组后的原子命题outside_ap，然后在prop_list中随机取样一个重组后的原子命题inside_ap，利用generate_from_list算法生成中序信号时序逻辑公式，按照模板三生成最终的信号时序逻辑公式，表示为：outside_ap+"-"+inside_ap+";"+generate_from_listprop_list； 在irregular_type=4时，随机取样一个重组后的原子命题，基于该重组后的原子命题，利用generate_from_list算法生成one_sentence；然后随机取样两个重组后的原子命题，基于该两个重组后的原子命题，利用generate_from_list算法生成生成other_sentence，从prop_list中随机获取一个重组后的原子命题ap，获取一个随机数sign，若随机数sign=0，则按照模板四生成最终的信号时序逻辑公式，表示为：ap+"-"+one_sentence+";~"+ap+"-"+other_sentence；否则，按照模板四生成最终的信号时序逻辑公式，表示为：ap+"-"+other_sentence+";~"+ap+"-"+one_sentence； 其中，type1_phrase是按照模板一中的不规范类型生成的一个简单句数据集type1_phrase，由重组后的原子命题的组合构成； 同样地，type2_phrase是按照模板二中的不规范类型生成的一个简单句数据集type2_phrase，重组后的原子命题的组合构成。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人南京航空航天大学，其通讯地址为：213300 江苏省常州市溧阳市滨河东路29号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。