公开(公告)号：CN103140838A

公开(公告)日：2013-06-05

申请号：CN201180047719.5

申请日：2011-10-25

Applicant: 株式会社日立制作所

Inventor： 近久真章 ,  市井诚 ,  野口秀人

IPC: G06F11/36

CPC classification number: G06F11/3608 ,  G06F11/3604 ,  G06F11/3624

Abstract: 本发明提供一种源代码转换方法和源代码转换程序，该源代码转换方法使用计算机将软件的源代码转换为检查代码，具有：输入软件的源代码的步骤；输入不同的多个转换规则的步骤；输入与处理性能相关的约束即非功能规则的步骤；用上述不同的多个转换规则和上述非功能规则将上述源代码转换为用验证工具的输入语言描述的非功能检查代码的步骤。

公开(公告)号：CN105408872B

公开(公告)日：2017-11-24

申请号：CN201380078502.X

申请日：2013-08-28

Applicant: 株式会社日立制作所

Inventor： 铃木康文 ,  新原敦介 ,  市井诚 ,  野口秀人

IPC: G06F11/36

CPC classification number: G06F11/3608 ,  G06F8/40 ,  G06F8/427 ,  G06F8/436 ,  G06F8/4436 ,  G06F8/72

Abstract: 通过符号执行进行针对由人工实施的重构的等价性验证时，能够不使计算量爆发，而迅速地进行。在验证源代码的等价性时，进行基于解析源代码而得的结构图的结构比较的验证和符号执行的验证这两种验证。并且，在通过基于结构图的结构比较能够判定为结构一致的情况下，不进行符号执行。此外，在进行基于结构比较的验证前，对于重构前后的各个源代码，根据对每个重构模式决定的正规化信息对结构图进行正规化，在重构正当时，调整为结构一致。并且，对将重构前后的各个结构图进行抽象化而得的图进行符号执行来进行验证，由此限定进行符号执行的位置。

公开(公告)号：CN103140838B

公开(公告)日：2015-06-17

申请号：CN201180047719.5

申请日：2011-10-25

Applicant: 株式会社日立制作所

Inventor： 近久真章 ,  市井诚 ,  野口秀人

IPC: G06F11/36

CPC classification number: G06F11/3608 ,  G06F11/3604 ,  G06F11/3624

Abstract: 本发明提供一种源代码转换方法和源代码转换程序，该源代码转换方法使用计算机将软件的源代码转换为检查代码，具有：输入软件的源代码的步骤；输入不同的多个转换规则的步骤；输入与处理性能相关的约束即非功能规则的步骤；用上述不同的多个转换规则和上述非功能规则将上述源代码转换为用验证工具的输入语言描述的非功能检查代码的步骤。

公开(公告)号：CN105408872A

公开(公告)日：2016-03-16

申请号：CN201380078502.X

申请日：2013-08-28

Applicant: 株式会社日立制作所

Inventor： 铃木康文 ,  新原敦介 ,  市井诚 ,  野口秀人

IPC: G06F11/36

CPC classification number: G06F11/3608 ,  G06F8/40 ,  G06F8/427 ,  G06F8/436 ,  G06F8/4436 ,  G06F8/72

Abstract: 通过符号执行进行针对由人工实施的重构的等价性验证时，能够不使计算量爆发，而迅速地进行。在验证源代码的等价性时，进行基于解析源代码而得的结构图的结构比较的验证和符号执行的验证这两种验证。并且，在通过基于结构图的结构比较能够判定为结构一致的情况下，不进行符号执行。此外，在进行基于结构比较的验证前，对于重构前后的各个源代码，根据对每个重构模式决定的正规化信息对结构图进行正规化，在重构正当时，调整为结构一致。并且，对将重构前后的各个结构图进行抽象化而得的图进行符号执行来进行验证，由此限定进行符号执行的位置。

公开(公告)号：CN103052943A

公开(公告)日：2013-04-17

申请号：CN201180038784.1

申请日：2011-08-08

Applicant: 株式会社日立制作所

Inventor： 市井诚 ,  近久真章 ,  野口秀人 ,  长野岳彦

IPC: G06F9/44 ,  G06F11/28

CPC classification number: G06F8/40 ,  G06F8/51 ,  G06F8/75 ,  G06F11/3604 ,  G06F11/3624

Abstract: 为了在软件的模型检查中，降低用模型检查器的输入语言描述检查代码的成本，存在将软件的源代码转换为检查代码的方法。因为用户只能选择单一的转换方式，所以存在抽象化水平的变更困难、用于追随源代码的设计变更的规则修正成本较高、用于用不同检查工具检查的规则修正成本较高等课题。本发明在将源代码转换为检查代码时，提供选择多个转换规则的单元，用户能够容易地变更抽象化的水平。此外，多个转换规则包括将源代码转换为中间形式的转换规则、在中间形式中进行抽象化的转换规则和从中间形式转换为检查代码的转换规则。