程序验证（共6篇）
程序验证 篇1
0前言
由于设备清洗维护不当或防尘管理不当, 在过去二十年间, 因实际的或潜在的交叉污染问题已从市场上撤回了大量的药品。这些事件对消费者产生了伤害, 也给制药企业带来了恶劣影响。过去检查官更注意检查青霉素类与非青霉素类药物之间的交叉污染、药品与甾类物质或激素之间的交叉污染问题。现在检查官更关注可以共用一条生产线生产的品种的交叉污染问题。由于法规要求, 青霉素类与非青霉素类药物之间的生产已经进行了物理隔离, 而制药技术的进步使同一品种批间差异非常小, 即使清洁不彻底不会有很大风险, 最大的风险就是同一生产线不同品种的交叉污染, 这也是本文重点。
1 验证的准备
1.1 成立验证小组
以设备所在部门为主成立验证小组, 指定小组组长一名, 成员一般包括质量管理人员、检验人员、部门管理人员、岗位操作人员。列明在小组内人员的分工, 质量管理人员负责监督、指导整个验证过程, 按照公司的各个规程进行, 及跨部门的协调;检验人员负责验证过程中的样品检测, 需要具体写清楚谁来检测什么项目;部门管理人员负责协调人员、资源以保证验证的顺利实施, 并审核验证是否合理充分, 这些人员基本上经验丰富, 在验证中的作用也是最关键的;岗位操作人员负责验证的实施。小组组长一般由管理设备的技术人员或有经验的管理人员担任, 负责全面工作, 验证过程一定要保证全员参与。
1.2 风险评估
验证小组成立后, 在进行验证之前应先进行风险评估, 通过风险评估确定验证的范围和程度。验证的范围主要是要弄清楚有几个品种共用, 共用的设备有哪些, 验证的程度主要是弄清楚清洁过程的各项参数, 清洁后的检查项目。
1.2.1 品种的评估
列出共线品种, 分析各品种的性质是否接近, 清洗方法是否一致。如果清洗方法一致, 则选出一个品种或中间体作为清洗目标物。如果清洗方法不一致, 则需要进行多个清洁验证。首先, 按照清洗方法进行分类, 在每类中选出一个品种或中间体作为清洗目标物。如果每一个品种或中间体的清洗方法都不一致, 则建议不共用同一设备。
评估的内容应包括溶解性、清洗难度、日剂量、毒性、产品稳定性等内容。方法就是将每一产品的参数同时列出, 逐项对比, 找出清洗目标物。
一般情况下, 下一产品则选择批量最小的或是日剂量最小的。如果能够得到日剂量的信息, 则选用日剂量的千分之一和批量的10ppm中最小的;如果不能得到日剂量信息的原料药或中间体, 则选用批量最小。
1.2.2 设备的评估
列出设备清单, 清单内容包括:设备的名称, 生产商, 编号, 型号, 材质, 用途等, 必要时应附图纸。连接管道应写明长度, 直径, 坡度, 几个拐弯及弯度, 有无死角等信息。
找出共用的设备有哪些, 各部分与物料接触的内表面积多少, 依据内表面积的比例可以得出各个设备的安全系数。找出设备或连接管道中最难清洁的部位, 即最难清洗点。通过系统影响性评估和关键部件评估确定关键设备、关键部件。
1.2.3 清洁过程的各项参数
清洁过程的参数一般包括但不限于如下内容。
(1) 脏物保留时间:设备使用完成后, 最长可放置多长时间进行清洗, 或者放置多长时间后必须清洗。 (2) 使用的水及清洁剂的名称、浓度、配制方法, 用量。如需要加热, 则需注明溶剂的沸点、温度、回流时间等。使用注射用水时必须注明水温。 (3) 压力。 (4) 清洗时间。 (5) 清洗角度。 (6) 清洗间隔。 (7) 清洗循环次数。 (8) 浸泡时间及溶剂用量。 (9) 气吹循环次数。 (10) 气吹时间。⑾气吹间隔。⑿清洗有效期。
1.2.4 可接受标准
可接受标准的确定要依据药品的性质、要求。例如:药品难清洗不能够完全淋洗干净, 则采用擦拭法取样、检测。药品需要检测微生物限度或微生物对药品影响很大, 则最终检测要检测微生物限度。一般情况下, 可接受标准包括以下几项: (1) 目测淋洗水澄清透明, 无可见异物。 (2) 目测设备内壁及最难清洗处无可见异物, 对于光线不好的设备要借助照明设备。 (3) 淋洗 (擦拭) 取样并检测化学残留, 微生物限度, 细菌内毒素。如果测定特定的产品残留不现实, 则可以选择其他的代表性参数, 例如:总有机碳 (TOC) 和电导率。
1.3 验证支持文件的确认
风险评估后, 根据风险评估结论, 建立清洁程序;如果已有清洁程序, 查看清洁程序是否能对风险评估中的风险。清洁程序一定要有对风险评估中列出的各项参数、最难清洗部位、清洁剂、完整可操作性强的清洁方法。
针对清洁目标物建立相应的分析方法, 并验证。
建立取样程序并验证。取样程序一般包括淋洗法取样、擦拭法取样, 对其进行验证, 计算各取样方法的回收率。取样回收率要求:淋洗法取样, 回收率≥95%;擦拭法取样, 回收率≥50%, 回收率的RSD≤20%。
2 验证的实施
准备完成后, 进入了验证的实施阶段, 先做好验证方案, 按其计划的内容逐步进行验证操作, 得出结论后, 对结论总结形成验证报告。
2.1 验证方案的内容
验证方案应至少包括:封面、验证方案起草审核审批表及修订历史记录、目录、正文。正文应包括但不限于如下内容。
验证目的;系统描述;验证范围;验证小组及职责;相关文件、SOI、SOP符合性确认;实验项目与可接受标准;验证实施方案 (使用仪器、仪表、试剂, 实施步骤) ;验证进度计划;数据分析要求;偏差分析要求;验证小结要求。
附录 (仪器、仪表校验证书, 危险品易燃易爆品使用注意事项;验证原始记录格式等) 。
2.2 培训
验证方案批准后, 验证小组长对验证成员进行培训, 所有操作人员都应参加与其相关的验证方案内容的培训, 该培训应有培训记录并作为验证文件的一部分。对验证项目培训包含两方面。
2.2.1 验证方案的培训
授课人针对培训内容进行现场提问检查培训效果, 并将提问提纲及答案归档备案。
2.2.2 现场操作的培训
以观察实际操作的方法考核培训效果, 授课人评判是否合格。
具体培训内容要求:培训实施部门和授课人应根据需求和岗位技能要求以及参培人知识技能水平确定具体的培训内容的深度, 不仅要包括操作步骤, 还应包括技术理论、工作原理等。授课人在实施培训前应确定培训目标, 培训结束后进行培训效果评估判断是否达到培训目的, 并填写培训总结表。
2.3 现场实施
对所有参与人员培训后, 验证小组组长要监督和参与整个验证的实施, 对关键的最差条件、关键步骤一定要在现场, 并尽最大限度的要求更多的人员参与。
2.4 验证报告
验证报告中至少包括:封面、验证报告起草审核审批表及修订历史记录、目录、正文。正文应包括但不限于如下内容:验证目的;系统描述;验证范围;实验项目与可接受标准;验证小组及职责;验证实施情况;相关文件、SOI、SOP符合性确认;数据分析 (包括风险是否降低了的分析) ;偏差分析及措施;验证结论;再验证周期;附录。
3 结语
验证过程中发生偏差或变更都要及时记录, 并按照相关要求进行评估对验证的影响, 并且一定要被批准后, 才能继续进行验证, 在此不再赘述。
清洁验证是防止污染及交叉污染的一个很有效的手段, 各国的法规和指南对此都有相关的规定。公司在制定验证主计划时, 一定要注意将设备列全。原则就是与产品接触的必须做清洁验证, 不接触的则不用清洁验证。同时注意在操作之前一定要对人员进行培训, 操作过程中要实时监控。
因为药品的生产设备千差万别, 由于篇幅的限制, 不可能在此一一详述, 本文对于发酵原料药的清洁验证程序是适用的, 但对其他设备清洁程序也是很好的参考。
在做验证时, 一定要融入自己的想法, 说出我是怎么想的, 为什么这样想, 依据是什么, 通过阐述我对问题的理解和解决方案来说服检查官接受我的意见, 为药品清洁验证的效果和药品的质量提供保证。
参考文献
[1]国家食品药品监督管理局药品认证管理中心.药品GMP指南·原料药分册[S] (2011) , 北京:中国医药科技出版社, 229-237.
[2]国家食品药品监督管理局.药品生产质量管理规范[S] (2010年修订) .
[3]EU GMP附录15:确认与验证[S].
[4]FDA清洁验证指南 (7/93) [S].Validation of cleaning processes (7/93) GUIDE TO INSPECTIONS VALIDATION OF CLEANING PROCESSES.
[5]APIC活性药物成分清洁验证指南 (2000) [S].Guidance on aspects of cleaning validation in active pharmaceutical ingredient Plants December 2000
[6]PDA技术报告[R]. (29, 49) .TR 29 Points to consider for cleaning validation TR 49 Points to consider for biotechnology cleaning validation.
[7]国家食品药品监督管理局药品安全监督司和药品认证管理中心.药品生产验证指南 (2003版) [S].北京:化学工业出版社, 2003.
[8]何国强, 陈跃武, 马义岭, 等.制药工艺验证实施手册 (2012) [S].北京:化学工业出版社, 230-256.
程序验证 篇2
基于演绎推理的形式验证是程序验证的一种重要方法。其核心是由程序员书写断言描述程序的性质, 然后根据某种方式对断言进行演算产生验证条件, 最后使用某个自动定理证明器来证明验证条件。该方法的程序验证原型系统非常多,但是到目前为止还没有可供工业界使用的产品问世。其主要原因是验证原型系统的能力受限于自动定理证明器的能力。 在研究程序验证的过程中,必须考虑如何提高自动定理证明技术,同时也应该研究如何减少对自动定理证明器的依赖。
本实验室设计并且实现了一个源码级验证工具 ——面向Pointer C的程序验证器原型(简称原型系统)[1,2,3,4]。原型系统对Pointer C语言程序进行自动验证,先对程序进行形状分析生成形状图,然后根据程序员书写的前后条件以及循环不变式通过最强后条件演算方式生成验证条件,最后交给自动定理证明Z3[5]证明。本文研究的主要内容是,在引入自定义谓词增强断言语言的表达能力的同时,怎样减轻因此产生的自动定理证明器的负担。
原有的原型系统中由于断言语言能力的局限, 很多易变数据结构的性质无法简明准确的表达。为此,原型系统引入自定义递归谓词来描述这些比较复杂的程序性质。程序员在写代码的过程中有时会用到递归谓词的归纳性质。但是这样做带来的问题是,Z3在证明验证条件的过程中无法发现这些归纳性质,从而造成验证条件证明失败。
为了自动定理证明器能顺利完成验证条件的证明,原型系统由程序员提供自定义谓词之间的归纳性质定理来帮助自动定理证明器证明。同时由于性质定理是由程序员提供的,其正确性无法保证。本文给出一种先对性质定理本身进行具体分析然后再结合结构归纳的方法,实现了性质定理的自动证明。
本文接下来的内容安排如下,在第1节里介绍Pointer C程序验证器原型系统中断言语言的设计以及为什么需要引入自定义谓词;第2节给出程序员需要提供性质定理的原因;第3节详细阐述如何具体实现性质定理的自动证明;第4节简单介绍当前原型系统的组成以及可以通过的验证实例;第5节的主要内容则是全文总结以及相关工作的比较。
1程序断言语言设计
验证系统原型的核心是程序断言语言的设计, 其主要验证对象是操作易变数据结构的指针程序, 而易变数据结构的特点是递归性。为了准确用断言表达易变数据的性质,直观的方法就是引入谓词。 引入谓词有两种机制,一种是系统内部建立固定谓词让程序员使用,但是这种不满足多变的程序性质和复杂的数据结构;另一种是由程序员自己定义谓词来满足程序性质多变的情况,这也符合自动定理器的功能在不断扩展的事实。本文中采用的就是自定义谓词的机制。
1.1自定义谓词
自定义谓词是程序员自己提供的用以描述程序的性质的谓词,最常见是递归定义的谓词,也称归纳谓词。其详细文法可以参考Pointer C的程序验证器原型相关的文献[1,2,3,4]。
例如有结构体定义为:
typedef struct node{int data; Node* l; Node*r;}Node;
现在定义一棵二叉排序树(Binary Sort Tree),它提供性质定理的原因;第3节详细阐述如何具体实现性质定理的自动证明;第4节简单介绍当前原型系统的组成以及可以通过的验证实例;第5节的主要内容则是全文总结以及相关工作的比较。需要三个归纳谓词一起定义,其形式为:
符号:=的左边是谓词的名字以及谓词的参数, :=的右边是谓词的定义。谓词gt表示对于指针p来说, p指向空或者p指向一棵二叉树,且x的数值大于这棵树上所有节点的data域的数值。此时我们发现归纳谓词中的指针p不再是指向一个单独的存储单元,而是抽象成为了一棵二叉树。p可以为空树,也可以有左子树和右子树。这是由归纳谓词的定义决定的, 谓词体右边出现的同名谓词可以继续按照谓词的定义展开。所以BST的含义是:p可以为空树;当p不为NULL时,该树的上所有父节点的数据域data值小于右子树根节点的data值大于左子树根节点的data值。
1.2自定义谓词在程序验证中的作用
自定义谓词除了能够定义复杂的数据结构性质之外,还可以根据程序的实际特点定义指针之间的关系,只有灵活应用自定义谓词,才能正确书写正确的函数前后条件和循环不变式。现在用二叉排序树删除根节点的函数(图1)来具体阐述这个问题。函数的谓词定义为:
谓词(1),(2),(3)一起定义了一棵二叉排序树, 而谓词(4)则表示p指向的二叉树上所有的节点的data值都小于q指向的树 上所有节 点的数据 。 而BST_seg(p,q)则表示从p指针到q指针之间的树段上所有数据的性质。
这些谓词的定义都是原型系统验证二叉排序树 (非空树)根节点函数需要的。二叉排序树删除了根节点之后,还需要保持该数据结构是一棵二叉排序树,所以函数在while循环语句中寻找中序前驱,然后将它的值替换根点,最后删除这个中序节点。所以这个函数的性质的前条件是p!=NULL BST(p), 它的后条件是BST(p)。同时在循环语句中,指针s在该树的左子树上向右前进直至找到中序前驱,所以它的循环不变式是BST(p->r) lt_all(s,p->r) lt(q->data,s) BST_seg(p->l,q) BST(s) ,表明了它在循环语句执行的过程中程序代码一定会满足的性质。
2程序员提供的性质定理
由上文可以看出,自定义谓词为程序验证提供了便利,基于原有的谓词文法我们已经可以方便写出函数的前后条件以及循环不变式。但是新的问题诞生了,前后条件以及循环不变式演算完毕生成的验证条件交给Z3时,自动定理证明器无法证明结果。 而发生这个情况的原因是自动定理证明器Z3没有推导谓词之间的归纳性质的能力。
虽然Z3无法发现归纳谓词之间的归纳性质,但是程序员自己可以给出归纳性质的定理辅助Z3证明。 对于图1的二叉树根节点删除函数来说,提供几个性质定理,自动定理证明器就可以顺利进行验证条件的证明。这些性质定理如下:
二叉排序树删除根节点函数的循环不变形状图为:
图2中形状不变图表示循环语句中程序维持的形状。现在以性质定理(c)来说一下,为什么验证条件的证明需要它们。当BST_seg(p,q)的展开情况不为不动 点的时候 , 是基于p - > r上的谓词 性质B S T _ s e g ( p - > r , q ) , 将其他谓 词的性质 按照p - > r指向节点定义序列段的左边加入该谓词,得到BST_seg(p,q)。
根据图2的循环不变图,我们可以看图1函数循环体里的赋值语句{q= s; s = s->r; }中看出s从根节点到右子树前进方向,已经遍历过的节点序列的性质和当前指针指向的节点性质,再加上尚未遍历的节点性质综合起来才能证明循环出口的验证条件。也许就是说B S T _ s e g ( p - > l , q ) 可以扩大 到BST_seg(p->l,q->r),正是性质定理(c)表达的意思。
这个分析过程,实际上就给程序员提供了一种如何书写性质定理的思路。程序员在写代码的过程中,清楚谓词在形状图上的含义,也清楚自己利用了谓词上哪些归纳性质。比如在该例子中,程序员知道二叉树删除根节点后的中序节点就是该树左子树上最底层最右边的点,所以并没有直接将这个节点替换根节点,而是利用它的值是左子树上所有节点的最大值这个归纳性质。程序员将这个性质交给Z3作为推导的条件,就可以证明循环出口的验证条件。同时,程序员也可以对形状上各个节点附带的谓词性质进行分析,就能很容易地发现验证条件的证明缺少哪些性质定理。
3性质定理的自动证明
一般情况下,定理证明不存在自动发现归纳证明步骤的通用算法。但是对于原型系统的性质定理来说,出现的参数变量个数少,指针参数的递归结构明确而且形状固定,可以通过对定理各个组成部分的分析得到归纳证明的方法。本文提供一种自动证明性质定理的分析方法,并且按照这种方法在原型系统中实现了性质定理的自动归纳证明。
另外,本文采用的归纳方法不是自然数归纳法, 而是结构归纳法。它的基本思路是假设在某一个集合上某个命题成立,证明某个包含这个集合的集合上这个命题成立。接下来详细介绍这种方法的思路和具体实现过程中的步骤。
3.1证明思路
该方法的基本思路分为三个步骤,最后一步是归纳证明,前两步是分析性质定理的结构。本节会根据第2节二叉排序删除根节点函数的谓词和性质定理具体分析证明过程。
第一步,分析谓词间的依赖关系与谓词的归纳方式。谓词的依赖关系就是指谓词是基于哪些谓词定义,谓词lt的定义谓词不依赖其它谓词,谓词 ( 4 ) l t _ a l l依赖谓词 ( 2 ) l t 。同时也很容易得到谓词 (5)BST_seg依赖谓词谓词(3)BST、谓词(2)lt和谓词 (1)gt。而谓词的归纳方式在静态检查谓词时就已经完成。它从谓词参数的定义出发,比如谓词lt和gt都只有一个指针变量,所以按照二叉树的结构归纳。 而谓词lt_all有两个指针变量,但是它的谓词体中, 只有第一个指针的路径有变化,说明此谓词按照第一个指针变元归纳,并且归纳的方式是按照二叉树的结构。同理,我们可以得到谓词BST_seg的归纳变元也是第一个指针,但是他的归纳方式不再是按二叉树的结构,而是只按照节点的右子树路径r指针进行归纳。
第二步,利用性质定理(引理)间的依赖关系。 原则上来说,定理应该是按照各个谓词的定义就可以独立证明,比如定理(a)、(b)。实际上,证明某一个相对复杂的定理可以将其他的引理作为前提条件, 这样可以减少复杂定理的证明步骤。比如引理(e) 依赖于引理(a),没有引理(a),它要进行两次归纳证明。确定引理之间的依赖关系没有像谓词之间依赖关系那样直观,几乎没有明确的办法。一种简单的方法是,证明任意一条定理时,都将其他的定理作为前提条件。
第三步,按照第一步的分析出来的归纳变元跟归纳方式对性质定理进行证明。其具体的操作分为3小步:
1)按照第一步分析得到的归纳变元和归纳方式进行归纳基始证明。证明失败原型系统报错,退出程序验证;
2)按照第一步分析得到的归纳变元和归纳方式形成归纳假设;
3)将该引理外的其他引理和上一小步的归纳假设都作为前提条件跟引理一起交给自动定理证明器证明。证明失败原型系统报错。
3.2性质定理的自动证明过程
性质定理的抽象语法定义为其中P的形式为Q的格。下面我们以定理(d)
为例介绍如何在原型系统中实现性质定理的自动证明。
第一步,检查P和Q的归纳变元,决定是否需要归纳证明。系统原型在进行性质定理证明之前,会对每个谓词进行检查得到它们的归纳变元。如何寻找归纳变元第2节中有介绍。这样我们得到P的归纳变元集合A与Q的归纳变元集合B,A={a1,a2..ah}, B = { b1, b2. . b1} ,其中ai和bj都是指针路径(格式为ptr->next或者ptr->l),不包括指针数据域路径(格式为ptr->next->data)。同时我们还需要P、Q的指针路径集合X和Y。显然指针路径也包含了归纳变元集合的元素,因为单个谓词的指针路径中不会都是归纳变元。对于定理(d)来说,A={m,n->r},B={m}, X={m,n,n->r},Y={m}。
此外,我们定义函数NUM(x)求解集合的元素个数。根据NUM(A)和NUM(B)的值,我们得到三种情况。P与Q都没有归纳变元,直接交给Z3证明;P与Q只有一边有归纳变元,直接证明交给Z3证明;P与Q都有归纳变元,到第二步。的左边和右边都有归纳变元,所以到第二步证明。
第二步,得到归纳变元与归纳方式。归纳变元应该是P和Q中归纳变元的交集R中的元素,但是R≠ A∩B,而是A和B的等价交集。这里等价交集的元素分两种情况,第一种是它们是同一个变量,另一种是指如果不为同一个变量时它们互为别名。别名的含义为两个指针指向同一个节点。
得到等价元素的算法如下:先定义P中的指针路径等式集合 {1,2..n},根据 ,我们可以得到若干个指针路径的等价群组{E1,E2..Em},每一个群组都应该包括一组相等的指针路径。现在我们需要知道{a1,a2,a3..ah}和{b1,b2..b1}是否有等价的元素。当它们等价时,它们的减去同样的后缀后,留下的指针前缀至少有一组同时出现在某一个Ei中。具体来说,有路径p->next->next->next和q->next->next,那么它有三组需要验证的指针前缀,是(p->next->next, q - > n e x t ) ,( p - > n e x t , q ) 和( p - > n e x t - > n e x t - > n e x t ,q->next->next)。指针路径p->next和q->l不可能等价, 因为p和q不是一种结构体指针。
得到归纳变元之后,我们要寻找归纳方式。按照之前的内容介绍,每个谓词的归纳方式都不同。 我们按照归纳方式最有限制的谓词来,归纳方式最有限制就是二叉树的不动点限制最多,或者归纳路径的数目最少。当然我们可能有多种不同的最有限制的归纳方式,我们就一一尝试,如果每一个证明结果都是错误,我们就对性质定理报错。根据以上方法,很容易得定理(d)的归纳变元是m,归纳方式是m->r。
第三步,证明归纳基始。这个过程就是按照谓词的不动点的定义化简性质定理,然后交给Z3证明。 化简得方式就是将不动点的定义直接合取P。定理(d)的归纳基始:容易得证。
第四步,归纳假设的生成。我们按照第二步得到的归纳方式,将性质定理里的归纳变元替换为归纳路径就是归纳假设。有几种归纳路径,就生成几个归纳假设公式。定理(d)只有一个归纳路径,所以归纳假设为:
第五步,将归纳假设,归纳基始,所有谓词定义和其他性质定理作为条件,将性质定理本身交给自动定理器证明。如果证明结果如果为false,原型系统退出。
4原型系统简介
研究小组设计并且实现了面向Pointer C语言的的程序验证原型系统(简称原型系统)。它的基本流程为以下三个步骤:
1)预处理阶段(编译器前端)。这个阶段处理Pointer C语言,包括词法分析,语法分析和类型检查。具体的过程是,对程序员的源程序(包括编程语言跟断言语言)进行词法分析和语法分析,生成符号表和抽象语法树AST。同时还要进行类型检查,类型检查类似于C语言。
2)程序分析阶段(形状系统):遍历(1)生成的程序的语法树AST,根据形状图逻辑的演算规则生成各个程序点的形状图,还要进行形状检查和得到循环不变图。
3)程序验证阶段(验证条件生成器):以函数为单位,根据程序员提供的函数的循环不变式和前后条件,按照最强后条件演算方法和专有逻辑形状图逻辑演算得到验证条件,最后将验证条件交给自动定理证明器证明。
现阶段原型系统已经可以通过以下程序的验证, 一种是不涉及易变数据结构的非指针程序,快速排序,二分查找,二叉堆(数组实现)等;另一种是涉及易变数据结构的指针程序(全部包含性质定理跟自定义归纳谓词),有序单(双)链表的插入删除,有序单(双)向链表逆置,有序单链表合并, AA树插入,平衡二叉树、二叉排序树、treap树和splay树的插入和删除。
对原有的原型系统来说中,通过验证的大多数实例都包含性质定理。系统在假设其正确的情况下对所有的实例进行程序验证,实际上这种验证结果并不可靠。而在本文的工作实现之后,现有的实例中所有的性质定理都通过了验证,之前原型系统通过的实例的正确性得到了保证。
5总结与相关工作比较
本文的内容主要是实现了当前所有包含谓词的测试用例里中性质定理的自动归纳证明。性质定理描述了自定义谓词之间的关系,它和自定义谓词一样由程序员自己提供,其目的是辅助自动定理证明器证明验证条件。自动定理证明器的局限性,使其在不提供性质定理的情况下,需要推导出归纳性质的验证条件证明失败。此外,自动定理证明器也不具备归纳证明的方法。本文通过对性质定理本身以及谓词的分析给出了一种自动证明归纳定理的方法。
近年来,还有很多其他的国内外实验室也在开发源码级的验证工具。比如,Veri Fast是一个可以验证C和Java程序的工具原型[6]。它为了提高表达程序性质的能力,允许程序员定义归纳数据类型(类似于结构体定义)及其上的递归函数,还有允许定义基于分离逻辑的谓词。递归函数跟本文归纳谓词的最大区别是,递归函数需要提供更多参数,实际表达含义可以一样。
Veri Fast和本文的验证工具还有一个区别就是, 程序中的定理证明由程序自己提供。因为这个证明过程在Veri Fast中就是一个函数。但是本文是原型系统的工作,程序员只需要根据形状图分析书写性质定理就可以了,难度相对会小不少。此外,Dafny[7]工具的最新实现[8]和本文方法的自动证明定理的方法很接近似。它和我们原型系统一样,提供性质定理,在Dafny中叫做lemma。同样对lemma进行归纳证明,不过它和我们原型系统不同的是,它作的是自然数归纳证明,并且允许多个变量归纳的情况。
还有其他一些类似于本实验原型系统的工具, 大多数验证工具都和原型系统一样,引入自定义谓词提高程序断言语言的表达能力,比如有[9,10]。但是这些工具都没有提供像本文中实现的自动证明性质定理的功能。而且这里面的某些工具,为了验证谓词归纳性质的方便性,在编程语言中限制了循环语句的使用,极大的降低了编程的灵活性。
参考文献
[1]ZHANG Zhi-tian,LI Zhao-peng,CHEN Yi-yun,et al.An Automatic Program Verifier for Pointer C:Design and Implementation[J].Journal of Computer Research and Development,2013,Vol.50(No.5):1044-1054.
[2]Zhaopeng Li,Yu Zhang,Yiyun Chen.A shape graph logic and a shape system.Journal of Computer Science and Technology.28(6):1063-1084,Nov.2013.
[3]XU Wen-yi,CHEN Yi-yun,LI Zhao-peng.Verifier Prototype for Programs with User-defined Predicates in the Assertion Language[J].Journal of Chinese Computer Systems,2013,Vol.34(No.7):1482-1486.
[4]SONG Yan-hui,LI Zhao-peng,CHEN Yi-yun.Automatic Inference of Pre and Post Shape Graphs for Pointer-type Recursive Functions[J].Journal of Chinese Computer Systems,to be published.
[5]Leonardo de Moura and Nikolaj Bjørner.Z3:An Efficient SMT Solver,Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS),Budapest,Hungary.Vol 4963 of LNCS,pages 337–340,2008.
[6]Bart Jacobs,Jan Smans,Pieter Philippaerts,Frédéric Vogels,Willem Penninckx,and Frank Piessens.Veri Fast:A Powerful,Sound,Predictable,Fast Verifier for C and Java.In NASA Formal Methods,pages 41-55,2011.
[7]K.Rustan and M.Leino.Dafny:An Automatic Program Verifier for Functional Correctness.In LPAR-16,LNCS 6355,pages 348-370,2010.
[8]K.Rustan and M.Leino.Automating Induction with an SMT Solver.In VMCAI 2012,LNCS 7148,pages 315-331,2012.
[9]W.-N.Chin,C.David,H.H.Nguyen,and S.Qin.Automated verification of shape,size and bag properties via user-defined predicates in separation logic.Science of Computer Programming,doi:10.1016/j.scico.2010.07.004,2010.
程序验证 篇3
为了确定分析室进行某些特定检测的能力，监控分析室的持续能力，识别分析室中的问题并制定相应的补救措施。2 范围
本程序适用于本分析室与其他实验室间进行的比对和能力验证试验；适用于实验室认可机构安排进行的能力验证试验。3 权责
3.1 实验室负责人主持比对和能力验证工作的开展，及对结果进行评价。3.2 实验室负责人制定实验室比对和能力验证实施计划。
3.3 比对和能力验证试验所涉及的本分析室岗位按照比对和能力验证试验计划要求，组织开展比对和能力验证试验。
3.4 资料管理员负责实验室比对和能力验证工作中有关资料的归档管理。4 定义
无 5 作业
5.1 比对和能力验证试验的方式
5.1.1 CNAS安排进行的比对和能力验证试验。对此类试验，本分析室均应积极主动参加，如当时确有实际困难无法参加时，必须以书面形式申请暂不参加；如果没有提出暂不参加申请或申请未被认可，不可无故拒绝参加。
5.1.2 本分析室自行组织的与外部实验室之间的比对和能力验证试验。5.1.3 实验室间比对和能力验证试验频次要求
5.1.3.1 实验室比对频次按“分析室品质管制活动计划”规定要求实施。
5.1.3.2 能力验证试验频次按“CNAS-RL02能力验证规则”和“CNAS-AL07能力验证领域
和频次表”文件要求执行实施。5.2 验证项目的选择
5.2.1 实验室认可机构下达的比对和能力验证试验计划所涉及项目。
5.2.2 本分析室自行组织的比对和能力验证试验，项目由质量、技术负责人共同商定，主要包括以下几方面内容：
客户投诉项目； 无法溯源的仪器设备； 新开展的检测项目；
使用非标准检测方法的项目；
其他技术水平要求较高或有必要的检测项目。
5.3 比对和能力验证试验的组织
5.3.1 明确比对和能力验证试验的任务后，由技术负责人联系参与比对和能力验证试验的外部实验室，安排比对和能力验证试验的时间，以及核算所需实验经费。
5.3.2 技术负责人编制比对和能力验证试验工作计划。计划内容主要包括：
比对和能力验证试验的项目；
参加比对和能力验证试验的外部实验室； 比对和能力验证试验的时间安排； 经费核算。
5.3.3 外部实验室的选择
本分析室一般优先选择以下实验室参与实验室间比对和能力验证：
质量管理体系符合ISO/IEC 17025要求，并经有关组织认可的实验室（如通过国家实验室认可的实验室）；
实验室间比对和能力验证项目应是该实验室经过认可的项目。
5.3.4 比对和能力验证试验工作计划需经分析室负责人批准后，方可实施。5.4 比对和能力验证试验的实施
5.4.1 实验室认可机构组织的比对和能力验证试验中，实验室负责人领取样品后，将其发给分析室分析检测。
5.4.2 本站组织的比对和能力验证试验中，由实验室负责人根据计划要求准备数份同样的样品，一份作为检测任务下达给本分析室分析检测，其它分送给参加比对和能力验证试验的外部实验室委托检测。
5.4.3 比对和能力验证试验任务下达到分析室后，由实验室负责人负责组织实施。5.4.4 参加比对和能力验证试验的检验人员在接到检测任务后，应以严谨的科学态度开展工作，包括检测环境的确认，仪器设备及有关消耗品的准备，检测过程的控制和检验结果的记录等。
5.4.5 检验人员完成比对和能力验证试验任务后，以化学分析报告的形式出具检验结果，交实验室负责人或技术负责人汇总。
5.5 比对和能力验证试验的总结
5.5.1 实验室负责人对本分析室返回结果和外部实验室的检测结果（或给定的参考值）进行分析比较，写成分析报告，并将相关资料汇总后，组织分析评审会议，召集有关
人员讲评比对和能力验证试验结果，当比对结果有差异时，要求有关岗位分析可能原因，提出进一步提高检验水平的具体措施。
5.5.2 实验室负责人综合评审内容，编写比对和能力验证试验总结报告。
5.5.3 比对和能力验证试验总结报告和其它有关资料由资料管理员整理，按照《记录管制程序》的要求，归档保存。
5.6 比对和能力验证试验结果的利用 5.6.1 对可接受的比对和能力验证结果
必要时，实验室应评价方法的偏移和精密度来确定比对和能力验证结果是否具有超
出或不可接受的高的概率；同时，评估结果比对的趋势或明显的趋向，是否能发现
其可提示或潜在存在的一些问题。
5.6.2 对不可接受或离群数值的比对和能力验证结果
当实验室的比对和能力验证结果报告为离群数值时，应组织相关人员对其检测的质控系统每一个方面全面进行评估，分析原因并及时予以整改；评估过程按文件
程序验证 篇4
ASP.NET与IIS、.NET框架和操作系统所提供的基础安全服务配合使用, 共同提供一系列身份验证和授权机制。ASP.NET的安全体系结构如图1所示:
二、ASP.NET安全访问技术[2]
(一) 验证 (Authentication)
身份验证是获取用户标识并验证标识的过程。在ASP.NET中主要用到三种验证模式, 且都在IIS身份验证之后。
1、window身份验证:
ASP.NET将依靠IIS对用户进行身份验证。Web客户的权限将与Windows用户和角色的权限相同。如果所请求的资源允许匿名访问, 则不进行身份验证;如果所请求的资源需要用户具有一定的权限, 则IIS将请求发送到ASP.NET程序去处理, 如果身份未通过或未被授权则拒绝访问。通过对Web.config的设置来启用这种认证:
2、表单窗体身份验证:
当用户向拒绝匿名访问的资源发出请求时, ASP.NET将客户端发送的未经验证的请求重定向到登录页面, 原始请求的URL被保存为URL参数以便以后使用。然后用户输入凭证, 提交页面, 应用程序根据数据存储对凭证进行身份验证, 如果应用程序认可了凭证, ASP.NET发出一个Cookie, 里面包括了一个有效身份票据, 然后用户被重定向到用户原始请求页面。当用户在同一个会话中再次请求受限访问页时, 请求头中将包含带有身份票据的Cookie以便再次验证;如果没有通过验证, 则用户被拒绝访问。对web.config文件修改如下:
forms属性指定认证时使用的cookie名和登录页面的URL, timeout设置cookie有效期, path指示发出cookie所用的路径。C r e d e n t i a l s配置段指定认证时的有效用户身份。PasswordFormat指定发送证件给服务器时使用的加密方法, 该属性取值可以是clear (不加密) 、MD5、SHA1。user元素的name和password属性分别为用户名和密码。
3、Passport身份验证:
由Microsoft提供的集中身份验证服务, 该服务为参与站点提供单一的登录程序和成员服务。它将ASP.NET与Microsoft Passport软件开发包 (SDK) 相结合, 将用户重定向到Passport站点, 通过Passport服务来检查用户的证件, 然后生成Cookie返回到客户端。
(二) 授权 (Authorization)
授权旨在确定通过验证的用户可以访问哪些资源, ASP.NET提供了两种授权方式:
1、文件授权[3]
文件授权由FileAuthorizationModule执行, 利用NTFS文件系统的访问控制列表ACL控制用户或组访问受保护的资源, 但验证方式必须是Windows身份验证。这种授权方式主要通过系统管理员对文件的权限设定来实现, 文件权限被存储在ACL中。当通过认证的用户试图访问Web服务器上的文件时Windows将检查相应的ACL, 以确定该角色或身份是否被允许读取该文件。
2、URL授权
URL授权是通过Web.config文件定义用户、角色、操作类型和指定文件或文件夹, 并将用户映射到特定的URL, 然后再利用URLAuthorizationModule确保调用者的凭证与定义的用户和URL映射相匹配的功能。在web.config文件中对授权和角色进行配置, 语法如下:
三、ASP.NET表单验证方案的安全[4]
在ASP.NET应用程序中, 窗体身份验证通常是最佳的选择。
(一) 系统说明
本系统由两个页面构成, 其中success.aspx是登录成功的页面, L o g i n.a s p x用于验证用户登录, 它包含:用户名txtUserName, 密码框txtPassword, 选择加密类型的下拉列表框d l l E n c r y T y p e, 登录按钮b t n L o g i n和显示错误信息的lblMessage。用户账号和加密后的密码保存在数据库UserInfos的Users表中, 包括userName、password、salt几个字段。ASP.NET支持MD5和SHA1两种加密算法。登录时, 首先根据用户的选择对输入的密码加密, 再从数据库中找出与用户名匹配的密码, 将两者进行比较。若一致则认为该用户为合法用户, 通过Session.Add记录用户信息, 显示用户请求界面, 否则将其强制引导回登录界面。
(二) 配置表单身份验证
(三) 选择加密算法对密码加密
ASP.NET可以方便地实现对密码的加密, 本例根据用户选择的加密类型和一个随机salt值来对密码加密, 然后存入数据库。
1、Salt值的函数
private static string CreateSalt (int size)
{R N G C r y p t o S e r v i c e P r o v i d e r r n g=n e w RNGCryptoServiceProvider () ;
Byte[]buf=new byte[size];rng.GetBytes (buff) ;
return Convert.ToBase64String (buff) ;}
2、创建加密函数
根据用户提供的密码、加密类型和salt值生成加密密码, 下面是具体的代码:
private static string CreatePassword (string pwd, string salt, string EncryType)
{string PwdAndsalt=String.Concat (pwd, salt) ;
switch (EncryType)
{case"SHA1":{Password=FormsAuthentication.HashPasswordForStoringInConfigFile
(PwdAndsalt, "SHA1") ;break;}
case"MD5":{Password=FormsAuthentication.
HashPasswordForStoringInConfigFile (PwdAndsalt, "MD5") ;break;}}return Password;}
(四) 通过数据库对用户进行验证
ASP.NET 2.O提供的Session对象用来存储特定用户会话所需的信息, 让后续的网页读取, 避免了在不同页面间传递信息的时候信息显示在地址栏中。[5]
(五) 测试应用程序
假定我们已注册了一个用户, 然后登录, 下面是登录按钮的触发事件代码:
四、结束语
本文讲述了IIS和ASP.NET应用程序的安全机制, 并用实例说明了基于窗体的身份验证的一些实现方法。虽然.NET框架自身有一些安全保护机制, 但对于要建造一个真正安全的ASP.NET应用程序是远远不够的, 我们还需要更深入地研究。
参考文献
[1]蔡群英, 黄镇建《ASP.NET安全策略的研究》.计算机与现代化[J], 2007.6;
[2]罗海涛, 李心广《ASP.NET Web应用程序安全策略》.微计算机信息[J], 2007.9-3;
[3]Mark minasi Christa Anderson Michele Beveridge《Windows Server2003从入门到精通》.电子工业出版社[M], 2004.6;
[4]陈浩《构建安全的ASP.NET Web应用程序》.乐山师范学院学报[J], 2006.12;
程序验证 篇5
软件事务内存(STM)[1,2,3]是基于软件的事务内存实现,近些年的研究[4,5,6]表明,STM不仅能有效利用现已大量投入使用的多核多处理器,而且有希望像垃圾收集器一样被广泛应用在现代编译器的开发中,为自动实现对共享资源的互斥安全访问提供运行时的支持,从而大大减轻程序员开发并发程序的负担。但STM算法通常采用乐观投机和细粒度并发的实现方式,算法思想十分精妙,可靠性难以保证。因此,研究STM并发机制的验证方法对提高并发软件的可靠性和安全性有重要意义。
Transactional Locking II(TL2)[7]是经典的基于锁的STM算法,它通过细粒度并发代码来实现事务的原子性。验证底层细粒度并发代码的正确性等价于证明它与高层抽象事务原子块间的上下文精化关系[8],即在任意的调用环境下底层代码产生的行为不会比原子事务的行为多。但该算法思想巧妙,验证难度很大。据作者所知,目前还没有在代码级上对TL2事务底层实现的验证工作。
本文基于TL2算法给出了一个典型的读写事务T(3行)对应的底层细粒度并发代码P(28行),使用基于依赖保证的程序模拟技术证明代码P是对事务T的一个精化实现,即在代码级上验证读写事务底层实现的正确性。
本文的主要贡献如下:应用程序精化技术完成了TL2事务的底层实现在代码级的验证,总结出了TL2算法中具体状态和抽象状态对应关系满足的不变式和基于时间戳的读集检验策略满足的不变式,为完成整个TL2算法在代码级的验证奠定了基础。
1 软件事务内存和TL2算法
STM是模拟数据库事务的并发控制机制来控制并行计算时的共享内存访问的一种技术,它是锁的一种替代机制。在STM中,一个事务指的是一段读、写共享内存的代码。这些读写操作在逻辑上是一个独立的单元,其中间状态对于其它的事务而言,是不可见的。与现在许多并发应用程序广泛使用的锁机制不同,STM通常采用一种乐观投机的并发控制方式:一个线程独立完成对共享内存的修改,完全忽略可能存在的其它线程,线程在日志中记录对共享内存的每一个投机的读写动作,然后根据日志中的记录进行共享内存的一致性检查,如果没有冲突就提交事务并更新共享内存,否则根据日志中的记录进行回滚,并重新开始一个新的事务。这种乐观投机的策略往往可以增加系统的并发度:任何线程无需等待一个资源,多个线程可以并发而且安全地修改同一共享数据结构的多个部分,从而实现共享数据结构的细粒度同步访问控制。
STM机制提供一些接口,主要包括以下几个重要接口:STM_begin()表示开始一个事务并完成对事务的初始化操作;STM_read(x)用于读共享变量x并更新读集;STM_write(x, buffer)将新的值写入写集buffer; STM_validate()用于冲突检测; STM_c o m m i t ( ) 用于提交 事务并更 新共享内 存 ;STM_abort()用于事务失败时进行回滚。图1左边表示“STM_atom{y=x+3}”,表示一个被原子执行的事务,而右边则是调用STM机制提供的接口进行程序变换后得到的运行时程序。
TL2和多数STM算法思想类似,采用“投机→检查→提交或回滚”的方式实现对共享数据的同步访问控制,它通过维护一个全局时间戳来完成对共享数据的一致性检查,并为每个事务存储单元额外添加锁和版本号两个域,事务在提交时会根据最新的全局时间戳来更新存储单元的版本号。因而事务可通过比较存储单元的版本号与全局时间戳之间的关系来判断共享存储是否已过时,是否需要回滚重新读取。事务对共享存储单元进行写入操作时,不是直接写入,而是写在一个缓冲区中,最后提交前才获取该单元的锁,最后提交时写入并释放锁。
图2是一个支持共享存储读写访问的原子事务。该事务中x和y是整型共享变量(事务共享存储),它们会被多个并发执行的事务同时访问。tmp是事务内部的局部整型变量,只能被当前线程访问。该事务提供给 程序员的 抽象行为 是原子地 执行STM_atom{}内的三行代码。
图4给出上述事务基于TL2算法的底层实现,可认为它是TL2算法对上述事务编译的目标代码。其中每个共享变量会被翻译成为一个结构体(如图3所示)。该结构体中,data保存与高层对应的值;ver是版本号;lk是底层共享结构体的保护锁,锁空闲时为0,被线程id获取后为id。代码中gt是全局时间戳,是一个可被多个并发执行的事务同时访问的整型共享变量。代码中的NAN类似C语言中的NAN,意思是“非数(Not a Number)”,在验证时表示某个变量的值是未定义的。
图4中,函数increment_and_fetch(>)原子地把全局时间戳gt加1并返回gt的新值。函数trylock(&x)非阻塞地获取结构体x的锁:如果锁空闲,便获取锁并返回0;如果锁已被占用,直接返回1。函数unlock(&x)释放结构体x的锁。
程序用fail作为指示标志,用来表示事务是否成功提交。当fail为1时,表示失败;当fail为0时,表示成功。程序主干部分由while循环构成。如果事务未成功提交,则fail为1,就继续执行循环体直至事务成功提交。
底层细粒度代码执行过程如下:首先将fail置为0(第3行)并进行STM_begin操作(第4~5行),读取全局时间戳并初始化各变量。之后对变量x进行投机读操作(STM_read):首先检查x的锁是否空闲(第6行),之后读取x的值保存在tmp中(第8行),再检查锁是否空闲、版本号是否小于等于rv(第9行)。读前和读后的这两次检查就保证了从开始执行事务至今,x未被其他线程更改。随后进行STM_write操作,将值存在缓冲区中(第10~11行)。之后尝试获取x与y的锁(第12~15行)。之后改变全局时间戳并且把这个新的全局时间戳记录在一个线程局部变量wv中(第17行)。在这以后执行STM_validate操作(第18行),再次检查x的版本号是否小于等于rv。如果有不符,则将fail置为1。这就保证了从开始执行事务至今,x的值未被修改。最后进行提交(STM_commit,第21~22行):把缓冲区内的值写入x和y,用wv更新版本号,并释放锁。整个过程存在很多检查,任意一次检查失败就把fail置为1并进行回滚。
验证TL2实现时,通常把实现事务的底层代码的每一步对应到高层事务代码的某一步上,即找到底层代码每执行一步时高层代码执行到的对应位置(高层代码可以不执行,也可以执行若干步),本文把这个对应位置称作“线性化点”。找到这些线性化点后,证明两层程序状态满足某个对应关系,而这个关系体现了两层程序状态的一致性,进而体现了实现的正确性。但验证难度很大。
首先,验证时很难确定底层代码每执行一步时高层代码执行到的对应位置。比如底层代码改变全局时间戳之后,就要进行STM_validate和STM_commit操作。大多数人直观地认为再次检查x版本号是否小于等于rv后的那个程序点或者提交过程中的某个子步是线性化点,和高层事务执行后的那个程序点对应。但是因为检查x版本号后,x就可被其他线程修改,这样高层执行事务代码后,高层x和底层x的值就不一致。这样就不能建立一个清晰的对应关系。另外线性化点也不能“简单地”放在再次检查x版本号这步之前,因为在检查完成后才知道是否可以提交,才能确定这个到底是不是线性化点。
另外验证时要指定在线性化点上高层程序状态和底层程序状态的对应关系。但是TL2算法实现的代码的粒度很细,因此这个对应关系非常微妙。大多数人很容易直观地以为这个对应关系可以表述为“如果一个共享变量的锁空闲,那么该共享变量在高层程序状态上的值和在底层程序状态上的值相等”。但这个对应关系无法描述如下情况:如果最后一次检查x的版本号后要进行回滚,那么即使已经获取了一个共享变量的锁,它在高层程序状态上的值和在底层程序状态上的值依然相等。
2 TL2事务的精化验证
如果要对STM的实现进行验证,那么就必须对其正确性有一个定义。目前有许多对STM正确性的定义,比如可线性化(linearizability)[9]、可串行化(serializability)[10]、不透明度(opacity)[11]以及其他几种变形。这些都是针对事务执行历史定义的,很难直接应用在STM代码级的验证上。最近Attiya等人使用上下文精化关系来刻画STM实现的正确性[8]。基于这个定义,如果一个原子事务的实现是正确的,那么该原子事务和实现这个事务的底层代码之间具有精化关系,即底层实现事务的代码在执行过程中表现出来的可观测行为不比原有事务在执行过程中表现出的可观测行为多。这个定义很直观,通俗易懂,可以在代码层面对事务内存的实现进行验证,所以本文采用这个定义来描述TL2实现的正确性。
图4实现事务的底层代码 (参见下页)
验证两个程序之间是否满足上下文精化关系可采用Liang等人提出的基于依赖保证的模拟技术(RGSim)[12]。这个技术可用于模块化验证两个并发程序之间的精化关系。验证时需要指定两个程序在执行时的依赖保证条件以及两个程序在执行时程序状态要满足的不变式。两个程序状态始终要满足这个不变式,这个不变式反映了两个程序状态之间的对应关系,也就体现了两个程序状态之间的一致性,进而体现了实现的正确性。验证精化关系时,要确定高层和底层代码的对应点(即线性化点),验证不变式在这些对应点上始终成立;同时要验证在程序执行过程中,每个指令的前后条件都在环境(由依赖条件指定)中始终成立。Liang等人提出的基于依赖
保证的向前向后模拟技术[13]扩展了RGSim,通过证明并发数据结构提供的并发操作满足上下文精化关系,来证明并发数据结构的可线性化性。采用这项技术验证程序A是程序B的精化实现时,需要模拟地执行A和B。A每执行一步,就要找B的对应点(即线性化点)。如果对应点确定,那么B执行到对应点,即B执行线性化操作到达线性化点。如果对应点不确定,此时就遇到了“疑似的”对应点,那么在此做一个尝试性的线性化操作,将线性化后的程序结果与未线性化的程序结果均记录在验证时使用的程序状态中。以后检查中,如果发现某个条件不满足,此前的线性化结果要被舍弃,那么就在程序状态中舍弃线性化后的结果。如果发现条件都满足,此前的线性化结果应该被保留,那么就在程序状态中舍弃没有线性化的结果。本文验证时就采用RGSim和基于依赖保证的向前向后模拟技术。
对于线性化点确定的代码,RGSim验证精化关系非常有效。为了降低验证的复杂性,本文在高层和底层中加入一个中间层,将高层代码转换为中间层代码,然后验证高层代码和中间层代码的精化关系,之后再验证中间层代码和底层代码的精化关系。在验证高层和中间层代码的精化关系时,因为高层和中间层的线性化点确定,所以采用RGSim。
首先将高层代码转换为中间层代码,如图5所示。表示中间层共享变量的结构体和表示底层共享变量的结构体类似,但只有data和lk两个域。函数lock(&x)获取结构体x的锁,如果这个锁被其他线程占用,函数便阻塞直至锁被本线程获取。函数unlock(&x)释放结构体x的锁。图5中的尖括号“< >”将若干语句包含在一起组成一条原子指令。中间层先原子地执行如下操作:获取x和y的锁并执行原始事务。之后逐一释放x和y的锁。
验证高层和中间层之间的精化关系时,依赖保证条件可根据操作语义得出,此处省略。用到的不变式是
此不变式中,对高层和中间层都存在的变量,用下标进行区别,H表示高层,M表示中间层。此不变式体现了高层变量和中间层变量应始终保持的一致性,即x与y两个共享变量在高层和中间层中的值始终相等,且高层和中间层对应的局部变量tmp的值始终相等。高层和中间层的对应点是:当中间层线程执行第一个原子操作时,高层线程执行事务;当中间层线程执行余下操作时,高层线程不执行任何操作。经过推导,高层和中间层的精化关系便可得到验证。
验证中间层和底层的精化关系时,因为线性化点不确定,采用基于依赖保证的向前向后模拟技术。首先考虑中间层代码和底层代码在执行时的线性化点:底层代码在用increment_and_fetch函数改变全局时间戳之后,中间层代码尝试性地进行线性化。在提交之前,底层代码要对读取的共享变量x进行再次检查。如果发现没有问题,就进行提交,同时保留中间层线性化后的结果,舍弃中间层没有线性化的结果;如果发现有问题,那么就需回滚,同时保留中间层没有线性化的结果,舍弃中间层线性化后的结果。
在验证中间层和底层的精化关系时,依赖保证条件可以根据操作语义得出,此处不再赘述。用到的不变式反映了算法的本质,是验证的关键,所以下文主要对不变式进行阐述。表示不变式时,对中间层和底层都存在的变量,用下标进行区别,M表示中间层,L表示底层。
首先阐述的是中间层和底层程序状态的对应关系满足的不变式,即TL2算法中具体状态与抽象状态对应关系满足的不变式。该不变式为
该不变式是说,如果一个共享变量在中间层或底层的锁空闲,那么它在中间层和底层的值对应相等。该不变式保证了中间层和底层共享变量的一致性。同时它也体现了引入中间层的必要性。为了看清这个问题,假设没有中间层,那么就需要讨论高层和底层状态的对应关系满足的不变式,这个不变式可以写作
假设底层代码投机执行时已获取了x和y的锁,但是在最后STM_validate检查中失败,必须回滚。回滚前,x和y的锁没有被释放,不变式的前提为假,因此不变式为真。回滚后,不变式的前提为真,要保证不变式依然成立,不变式的结论必须为真,但这个是无法推导出的。在加上中间层后,就可以解决这个问题。在中间层尝试进行线性化操作后,程序状态中有两种结果,一种是线性化后的结果,一种是没有线性化的结果。如果在STM_validate检查中失败,那么就要保留没有线性化的结果。在这个结果中,回滚前,由于不变式成立,并且中间层的锁空闲(即不变式的前提为真),所以不变式的结论为真;回滚后,不变式的前提依然为真,回滚操作不改变共享变量的data域,这就使得不变式的结论依然为真,所以不变式依然为真。因此加入中间层后,这个不变式就能恒成立。
另外一个重要的不变式是基于时间戳的读集检验策略满足的不变式,这个不变式为
它的意思是如果1)共享变量x已经通过了初次检查并读取了x的值,并且2)x的锁在中间层或底层空闲,并且3)x的版本号不大于rv,那么读取x时保存值的局部变量tmp和对应的底层共享变量x的值相等。在读取x前的那次检查可使得条件1)成立,读取x后的那次检查可使得条件2)和3)成立。因为共享变量的版本号单调增加,所以只要在任意程序点条件3)成立,那么在这个程序点之前它始终成立。因此如果读取x之后的那次检查没问题,那么在读取x前检查锁的时刻以及读取x的时刻,条件3)都成立。这个就可以保证读取的x的值正确。类似地,也可以推导出在STM_validate时,如果通过了检查,读取的x的值正确。
最后还有一个不变式比较重要,这个不变式是
它是说线程局部变量rv和共享变量的版本号都始终小于或等于全局时间戳,这反映了全局时间戳单调增加的性质。在验证时这个不变式是一个重要的辅助。
采用基于依赖保证的向前向后模拟技术进行验证时,根据操作语义推导出每个语句在执行过程中的前后条件,同时验证这些前后条件在环境(由依赖条件指定(中始终保持。推导后便验证了中间层和底层的精化关系。
在验证高层和中间层的精化关系以及中间层和底层的精化关系之后,根据精化关系的定义,便可知高层和底层之间也有精化关系。这样便在代码级上完成了对这个TL2读写事务底层实现的精化验证。
3 相关工作
已有的许多工作[14,15,16,17]使用模型检查(modelchecking)验证STM算法,但为了减少状态数量并简化验证,他们的抽象模型通常将STM算法的若干步合为一个原子指令,这样就忽略了真实的STM算法在线程交叉执行时的微妙状态。而本文在代码级上对TL2事务的底层实现进行验证,并关注了这些微妙状态,同时还给出了这些状态对应关系满足的不变式。
Tasiran[18]对STM算法在代码级上进行了精化验证,但所验证的STM算法的策略与TL2的策略不同,所以所用方法不适用于TL2的验证。Mohsen等人[19]基于模拟技术提出了验证STM的框架,但只支持向前模拟,不支持向前向后模拟,也无法验证TL2事务的实现。而本文采用向前向后模拟技术验证了TL2事务的底层实现。
4 结束语
本文用TL2算法实现的代码具有代表性,体现了TL2算法的本质,帮助人们对TL2算法有更深入的理解。
引入中间层后,本文使用基于依赖保证的向前模拟技术(RGSim)验证了高层和中间层的精化关系,再使用基于依赖保证的向前向后模拟技术验证了中间层和底层的精化关系。这样便验证了高层和底层的精化关系,完成了对一个典型读写事务基于TL2算法的底层实现在代码级的验证工作。
程序验证 篇6
目前,循环程序的完全终止性问题是程序验证领域的一大核心和热门问题。具体来说程序终止是指,如果循环程序对于所有能进入循环的初始值都是终止的,则称该程序是终止的;如果循环程序对于某一个初始值是不终止的,则称该程序是不终止的。
一般来说,循环程序的终止性是不可判定的[1],但就某些子类的程序,其终止性是可以验证的。Tiwari已经在文献[2]中证明了一类线性循环程序的终止性是可判定的,并给出了相应的判别方法,夏壁灿、杨路等[3]利用符号的判定算法对其进行了补充和完善。但是在非线性循环程序的终止性方面,还没有多少确定的结果。文献[4]通过对最小、最大不动点的讨论,研究了一类多项式赋值函数在特殊区间上的终止性。最近,姚勇在文献[5]中证明了单变量的赋值函数在闭区间上的非线性循环程序是不终止的当且仅当赋值函数在此闭区间上有不动点,并且给出了当区间是开区间或者半开半闭区间时的判定算法。牟琳等[6]在此基础之上研究了一类特殊的,满足一定约束条件下的多区间的非线性循环程序的终止性。总的来说,从种种迹象表明,非线性循环程序的终止性与动力学中离散映射的不动点以及周期点之间具有十分紧密的联系,如何利用相关结论对非线性程序的终止性进行验证应该是目前研究的一个重要方向。但是即使是一维的简单情况,由于周期3蕴含混沌,也使得非线性程序在多区间上的终止性验证变得极为困难,所以在多区间上的非线性程序验证方面的任何研究进展都具有一定积极的意义。
在本文中, 我们利用一维离散映射的周期点的转换图方法以及符号动力学中相关的一些结论(如引理1和引理2),主要考虑了形如P1的一维非线性循环程序的终止性:
其中,Ω⊆R是有限个不相交的有界闭区间的并,即:
且(ai,bi)∩(aj,bj)=ϕ,i≠j
f:R→R,即f(x)是R上的一元连续函数。
1 相关概念和引理
在动力学中,一维离散映射是如下一维迭代函数:
其中n是非负整数,f是一维连续函数,xn是迭代变量。
显然,不考虑循环条件时,通过程序P1中的赋值函数产生的循环变量值序列就是一维离散映射所得的迭代变量值序列,所以二者在本质上是相同的。那么有关一维离散映射的许多相关结论都可以借用过来以分析程序P1的终止性。
如果∃x*,使得x*=f(x*),则称x*为函数f的一个不动点;如果∃x*,使得x*=fn(x*),则称x*为函数f的n-周期点(n>1),其中表示函数的n次迭代。
将各区间作为节点,如果有f(Ii)⊃Ij,(i,j=1,2,…,n),则从Ii到Ij有一条有向边,这样就可以建立函数f和区间Ii的有向图,并称该图为函数和区间的转换图[7]。
例1 如果函数f和区间I1,I2,I3有f(I1)⇔I3,f(I2)⇔I1∪I2,f(I3)⇔I1,则可得此函数和区间的转换图如图1所示。
下面的引理1、引理2和引理3都是符号动力学中的相关结论,下面仅给出引理3的证明,其余的详细证明请查看文献[7]。
引理1 设f是从闭区间[a,b]到R的一个连续映射,若f([a,b])⇔[a,b],则f在[a,b]上有不动点。
引理1体现在转换图上,即为节点自身有圈这种情况,如例1中I2,所以函数f在闭区间I2上存在不动点。
引理2 设I1=[a1,b1],…,IN=[aN,bN]是满足(ai,bi)∩(aj,bj)=ϕ,i≠j的有限个闭的且有界的区间,si∈{1,2,…,N},i=0,1,…,且si≠sj,i≠j,f:R→R,如果:
且Isn=Is0,那么Is0Is1…Isn形成一个圈,则函数f在区间
引理2体现在转换图上,即为由节点间的有向边可以构成圈这种情况,如例1中有圈I1I3I1,所以函数f在I1∪I3上有周期点存在。
引理3 设f是R上的一个连续函数,且f在闭区间[a,b]⊆R上有周期点,则f在闭区间[a,b]上必有不动点。
证明:因为周期为1的周期点即为不动点,此时结论显然成立,所以下面仅考虑设f有周期大于1的周期点的情形,令x1<x2<…<xp(p>1)是周期轨道上的点,其顺序是以其在数轴上的顺序来确定的。令i是满足f(xi)>xi的最大下标,则f(xi+1)≤xi,且f([xi,xi+1])⊃[xi,xi+1],由引理1可得f在[xi,xi+1]上有不动点。
2 主要结论
定理1 设[a1,b1],…,[aN,bN]是满足(ai,bi)∩(aj,bj)=ϕ,i≠j的有限个不相交的闭区间, 那么程序P1是不终止的,当且仅当赋值函数f在
证明:充分性显然成立,只考虑必要性,下面用反证法证明。假设赋值函数f在闭区间Ω上不存在不动点,也不存在周期点,可将区间Ω划分成有限的n个小区间:
则迭代路径可以表示为:
其中si∈{1,2,…,N},i=0,1,…。
因为程序没有不动点,由引理1可知其中任意路径中不会出现f(Isi)⊃Isi;
又因为程序没有周期点,所以由引理2得任意路径f(Is0)⊃Is1,f(Is1)⊃Is2,…中也不会有圈形成,即不会出现Isi=Isj;
而程序是不终止的,所以存在无限长的路径,并且其中无圈,即标号将无限且不重复的出现,即s0→s1→…,但因为区间的划分是有限的,所以标号不可能无限的且不重复的出现,所以假设错误,即如果程序是不终止的,则赋值函数f在Ω上存在不动点或者存在周期点,证毕。
由定理1和引理3容易得到与文献[5]中推论1一致的推论:
推论1 如果程序P1中的区间Ω=[a,b],那么程序P1不终止的充要条件是赋值函数f(x)在闭区间[a,b]上有不动点。
3 算法和例子
依据前面的引理和定理1,我们给出算法TNPCI (Termination of Nonlinear Programs over Closed Intervals)以验证程序P1的终止性:
算法TNPCI 有界闭区间上的非线性循环程序的终止性验证算法
输入:循环程序的循环赋值函数和循环区间。
输出:如果程序是终止的,输出T;如果程序是不终止的,输出NT。
Step1 计算各区间的长度
Step2 找出分割后的各区间的映射情况,构造函数和区间的转换图,删掉循环条件区间以外的区间和相应的边;
Step3 检查转换图,如果有圈存在,即有周期点或不动点存在,程序不终止,则返回NT,否则下一步;
Step4 如果转换图中无圈存在,检查区间端点是否构成周期点,若构成则程序不终止,返回NT,否则程序终止,返回T。
可以看出算法TNPCI对于赋值函数在循环区间上具有周期点(包括不动点)的循环程序来说,不用求解不动点和周期点,就能对其终止性进行验证,这一点比文献[5]的算法要好。
下面我们以例2演示算法TNPMI的算法步骤,之后用该算法验证文献[5]中的P6的终止性:
例2 while
end
其中
Step1 因为
Step2 那么分割出的小区间的映射情况为:
可得构造函数和区间的转换图如图3所示。
再删掉循环条件以外的区间即删掉L3及其上的边,得转换图如图4所示。
Step3 转换图存在长度大于1的圈L2L4L2。所以此程序不终止,返回NT。
注意:这里已经存在长度大于1的圈,所以可以验证此程序是不终止的,而没有验证端点情况。但实际上这里的端点
在文献[5]中,程序P6的终止性不能得到验证,而用本文提出的算法可以容易验证程序P6是不终止的。实际上程序P6和本文前面的例2类似,只是考虑的区间长度更小,所以利用算法TNPCI时只需要将区间划分得要更细一些就可以解决了。
例3 文献[5]中的P6
Step1 因为
所以
Step2 找出各区间的映射区间,并删掉循环条件区间以外的区间,即(i=1,2,…,9):
Step3 容易得到这里的转换图存在长度大于1的圈,如图6中的L1L11L20L1,所以程序是不终止的,返回NT。
4 结 语
本文赋值函数是一维连续函数、循环条件是有限个内部不相交的有界闭区间并的非线性循环程序的终止性进行了验证。我们的算法对于形如P1的含有周期点的非线性循环程序的终止性验证特别适用。但由于这种算法要求程序的循环区间是有界闭区间,那么对于含有无界区间或开区间的情况该怎么处理就是紧接着可以考虑的方向。
此外,在一维赋值函数的基础上可以继续研究二维或更高维的情况;又或者仍然是一维的,研究含分支的循环程序的终止性,其实本文中的例1和例2,因为赋值函数是分段函数,所以是可以改写为含分支的循环程序。可想而知,一维的含分支的循环程序应该可以用分段函数的形式表示,但是函数可能不再保持连续,所以对于含分支的循环程序的验证还是会有困难。接下来也可以在这个方向上继续研究。
还有就是算法设计上,我们的算法针对某些特殊情况的效率可能不高,可以结合文献[5]和文献[6]中关于特殊情况下的算法重新设计,使得算法针对不同情况的算法效率更高。
摘要：利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法。利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性。最后,给出计算实例演示该算法的算法步骤。
关键词：程序验证,终止性分析,非线性循环程序,不动点,周期点
参考文献
[1]Alan Turing.On computable numbers,with all application to the ents-cheidungs problem[J].London Mathematical Society,1936,42(2):230-265.
[2]Tiwari.Termination of linear programs[C]//Proceedings of the Com-puter Aided Verification,Lecture Notes in Computer Science,2004,Volume3114,2004:70-82.
[3]Bican Xia,Lu Yang,Naijun Zhan,et al.Symbolic decision procedure for termination of linear programs[J].Formal Aspects of Computing,2011,23(2):171-190.
[4]Babic D,Hu A J,Rakamaric Z,et al.Cook.Proving Termination by Divergence[C]//Proceedings of the fifth IEEE International Confer-ence on Software Engineering and Formal Methods.London,2007:93-102.
[5]姚勇.区间上非线性程序的终止性判定[J].软件学报,2010,21(12):3116-3123.
[6]牟琳,李轶,李玲娜,等.多区间上非线性程序的终止性判定[J].四川大学学报:工程科学版,2011,43(3):76-80.
[7]罗宾逊.动力系统导论[M].韩茂安,等译.北京:机械工业出版社,2007.
[8]Bradley A,Manna Z,Sipma H.Termination analysis of integer linear loops[C]//Proceedings of the Concurrency Theory,Lecture Notes in Computer Science,2005,Volume3653,2005:488-502.
[9]Yang L,Zhou C,Zhan N,et al.Recent advances in program verifica-tion through computer algebra[J].In Front.Comput.Sci.China,2010,4(1):1-16.
[10]Yang L,Zhan N,Xia B,et al.Program verification by using DISCOV-ERER[C]//Proceedings of the VSTTE’05held in Z¨urich,Oct.10-Oct.13,2005.