公开(公告)号：CN109766268B

公开(公告)日：2019-10-25

申请号：CN201811543051.3

申请日：2018-12-17

Applicant: 南瑞集团有限公司 ,  南京南瑞信息通信科技有限公司 ,  国网江苏省电力有限公司南通供电分公司 ,  国家电网有限公司

Inventor： 祁龙云 ,  杨维永 ,  刘苇 ,  路红 ,  吕小亮 ,  魏兴慎 ,  李云鹏 ,  唐伟 ,  周峰 ,  朱世顺 ,  闫珺

IPC: G06F11/36

Abstract: 本发明公开了一种顺序汇编指令程序的验证方法与系统，其中方法包括：对每一条汇编指令建立一个语义规则；依次读取每一条汇编指令，获取每一条指令的所有的操作数，并记录每个操作数的地址、操作数的初始数值和长度；对程序的所有指令依次将所有操作数‑的数值规约为它们的初始值的表达式；对于每一条指令按照顺序依次根据相应的指令语义规则，生成相应的证明脚本。本发明方法从比较简单的汇编指令的语义规则、简单的单条汇编指令的语义证明脚本的生成方法出发，利用归纳技术方法得到整个顺序汇编指令程序语义的规约和验证脚本生成的方法，可以大大减少形式化工作的工作量。

公开(公告)号：CN109766268A

公开(公告)日：2019-05-17

申请号：CN201811543051.3

申请日：2018-12-17

Applicant: 南瑞集团有限公司 ,  南京南瑞信息通信科技有限公司 ,  国网江苏省电力有限公司南通供电分公司 ,  国家电网有限公司

Inventor： 祁龙云 ,  杨维永 ,  刘苇 ,  路红 ,  吕小亮 ,  魏兴慎 ,  李云鹏 ,  唐伟 ,  周峰 ,  朱世顺 ,  闫珺

IPC: G06F11/36

Abstract: 本发明公开了一种顺序汇编指令程序的验证方法与系统，其中方法包括：对每一条汇编指令建立一个语义规则；依次读取每一条汇编指令，获取每一条指令的所有的操作数，并记录每个操作数的地址、操作数的初始数值和长度；对程序的所有指令依次将所有操作数-的数值规约为它们的初始值的表达式；对于每一条指令按照顺序依次根据相应的指令语义规则，生成相应的证明脚本。本发明方法从比较简单的汇编指令的语义规则、简单的单条汇编指令的语义证明脚本的生成方法出发，利用归纳技术方法得到整个顺序汇编指令程序语义的规约和验证脚本生成的方法，可以大大减少形式化工作的工作量。