公开(公告)号：CN114647414A

公开(公告)日：2022-06-21

申请号：CN202011510721.9

申请日：2020-12-18

申请人： 北京广利核系统工程有限公司

发明人： 杨晨 ,  江国进 ,  彭立 ,  马建新 ,  张春雷 ,  张智慧 ,  谷伟卿 ,  任保华 ,  张雁

IPC分类号： G06F8/41

摘要： 本申请公开了一种应用软件增量编译方法、装置和计算机设备。其中，应用软件增量编译方法包括：接收增量编译的操作请求；判断操作请求是否满足增量编译条件；如果满足增量编译条件，则构建变量存储信息表；基于变量存储信息表对应用软件进行增量编译。本申请实施例的应用软件增量编译方法、装置和计算机设备，通过接收增量编译的操作请求，并在满足增量编译条件时，构建变量存储信息表，以及基于变量存储信息表对应用软件进行增量编译，对增量编译次数无限制，无新增物理文件，对系统性能无影响。

公开(公告)号：CN103646194A

公开(公告)日：2014-03-19

申请号：CN201310631729.4

申请日：2013-11-29

申请人： 北京广利核系统工程有限公司 ,  中国广核集团有限公司

发明人： 张雁 ,  杨晨 ,  任保华 ,  张智慧

IPC分类号： G06F21/12 ,  G06F17/30

CPC分类号： G06F11/3608

摘要： 本发明公开一种基于形式化验证的同步数据流程序的可信排序方法，包括Lustre并行程序和由Lustre并行程序排序后得到的串行C程序，通过对任意两个满足拓扑排序的Lustre程序，证明其拓扑排序前的Lustre程序和拓扑排序后的Lustre程序执行语义等价，得到排序后的C程序与排序前的Lustre程序在语义上执行等价。本发明以“入度为零的顶点拓扑排序算法”为理论基础，基于形式化语言进行开发实现，通过对任意两个满足拓扑排序性质的程序在串行语义中执行是等价的证明，在形式化验证时考虑了并行语言在转化成串行语言过程中的所有情况，并分别对每种情况都做了证明，得到排序后的程序满足拓扑排序的性质，从而保证方案的正确性，提高整个软件系统的安全性和可靠性。

公开(公告)号：CN103646194B

公开(公告)日：2016-04-06

申请号：CN201310631729.4

申请日：2013-11-29

申请人： 北京广利核系统工程有限公司 ,  中国广核集团有限公司

发明人： 张雁 ,  杨晨 ,  任保华 ,  张智慧

IPC分类号： G06F21/12 ,  G06F17/30

摘要： 本发明公开一种基于形式化验证的同步数据流程序的可信排序方法，包括Lustre并行程序和由Lustre并行程序排序后得到的串行C程序，通过对任意两个满足拓扑排序的Lustre程序，证明其拓扑排序前的Lustre程序和拓扑排序后的Lustre程序执行语义等价，得到排序后的C程序与排序前的Lustre程序在语义上执行等价。本发明以“入度为零的顶点拓扑排序算法”为理论基础，基于形式化语言进行开发实现，通过对任意两个满足拓扑排序性质的程序在串行语义中执行是等价的证明，在形式化验证时考虑了并行语言在转化成串行语言过程中的所有情况，并分别对每种情况都做了证明，得到排序后的程序满足拓扑排序的性质，从而保证方案的正确性，提高整个软件系统的安全性和可靠性。