摘要：提出基于实体模型的三维几何公差标注正确性自动验证方法。介绍了基于几何要素自由度分析的公差标注正确性验证的原理,讨论了三维公差标注可能存在的错误及相应的验证规则。提出了基于SolidWorks软件的三维公差标注正确性验证软件的总体设计架构,研究了相关程序算法,并给出了基于三维实体模型的几何信息和公差标注信息的数据提取方法。通过设计实例零件和错误标注案例,验证了软件的设计思想和算法的正确性。

摘要：为保证高炮动态射击诸元标准值程序能够在动飞试验前保证正确性,应用开放-封闭原则建立算法和适用于此算法的测试流程。算法基于所建立的中介坐标系,通过抽象出不同射表的通用接口,区分开程序中变化部分与不变部分,将算法复杂度从动态解题难度简化到静态解题难度;通过在不同试验间共享测试过程,使依此算法编写的程序不变部分和变化部分都可以在动飞试验前经过实际试验的检验。在多种高炮武器系统定型试验中的应用表明,此种方法可以在动飞试验前保证程序的正确性。

摘要：联邦学习作为一种新兴的分布式机器学习技术,允许用户通过服务器协同训练全局模型,而无需共享其原始数据集.然而服务器可以对用户上传的模型参数进行分析,推断用户隐私.此外,服务器还可能伪造聚合结果,诱导用户发布敏感信息.因此用户需要对参数进行保护,同时对聚合结果进行正确性验证.本文设计了一种可验证的联邦学习方案.首先,基于公开可验证秘密共享设计了双掩码安全聚合协议,在保护用户模型参数的同时还能支持用户的动态退出和共享验证功能,确保服务器解密的正确性.其次,基于同态签名构建验证公钥更短的聚合结果验证方案,使用户可以验证服务器聚合结果的正确性.实验结果表明,同现有方案相比,方案验证聚合结果时的计算开销和通信开销同时处于较低水平.安全性分析证明了方案在隐私保护方面能够有效防止恶意攻击和数据泄露,保障了联邦学习训练的安全性.

摘要：自动检测与验证HMSC(high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义,为此提出一种为HMSC模型进行自动检验的方法,并将其实现。利用转换规则为HMSC模型生成Promela检测语言,借助SPIN工具对需求进行验证。该方法不仅支持模型检测,同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具,通过一个实例展示其自动建模检测分析的效果,表明了其有效性和实用性。

摘要：由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域,并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性,达到对系统功能实现的正确性验证.同时,使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型,基于这一形式化模型,在Isabelle/HOL中验证系统模块的功能语义的正确性.以实现的安全可信OS(verified secure operating system,简称VSOS)为例,阐述了所提出的形式化设计和验证方法,说明了这一方法的可行性.

摘要：为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法。针对于Hoare公理化方法证明中的前置条件难以寻找的问题,提出了将这两种演算方法结合使用的方法。对最弱前置谓词变换法的过程进行分析,确定了最弱前置谓词算法的准确性。将最弱前置谓词应用到公理化方法中,即把最弱前置谓词变换法求出的前置谓词作为公理化方法的前置条件。通过一个具体实例,详细说明了其验证过程,并证明了该方法的有效性。

摘要：在对当前面向服务体系架构(service-oriented architecture,简称SOA)研究的基础上,给出了一个以企业服务总线(enterprise service bus,简称ESB)为中心的面向服务软件体系架构参考模型(SOA reference model,简称SOARM),是集Petri网和时序逻辑于一体的形式化SOA分析、验证和确认方法.基于以客户为中心的面向服务架构设计理念,即根据用户提出系统规范/需求,服务提供者提供服务或组合服务来满足服务消费者,服务接口和ESB作为实现面向服务架构的关键部分.虚拟计算环境下,服务语义的一致性验证是十分必要的,SOARM采用新的模式:通过Petri网为服务的行为建模,时序逻辑来描述服务语义一致性约束,综合运用分而治之的精炼检测思想和SOA模型检测合成方法,通过对这些子服务性质的检验来验证整个系统的规范.用商业银行综合前置系统说明了如何使用这种方法来实现面向服务的设计.

摘要：为确保以导航星座星间链路为代表的复杂星间链路的运行服务效果,在使用网络建链拓扑、路由规划参数前,应对其正确性和有效性进行评估确认.本文提出了对复杂星间链路网络规划进行参数正确性快速评估和业务服务性能评估的分级评估方法.第一级评估实现网络规划结果正确性的快速判断,涵盖了场景要素符合性、节点特性符合性、测量业务约束满足性、数传性能满足性等多维度综合化快速验证评估.第二级实现网络规划结果有效性的进一步确认,构建由星间网络行为模型和数据接入模型组成的星间链路网络仿真系统,基于星间数据传输和处理的加速仿真,统计建链数量和数据包传输性能并与业务服务指标比对,完成业务服务性能仿真评估.经对导航星座星间链路典型业务场景的两级评估结果的比对,验证了分级评估方法的有效性.

摘要：设计了一个基于Petri Net的Web服务组合流程建模引擎.把BPEL流程的语法元素按其语义转换为Petri Net模板,通过模板组合来得到整个流程的Petri Net模型,并以Petri Net标记语言(Petri Net Mark-up Language,PNML)文件格式来描述Petri Net模型,从而能够利用现有的支持PNML文件的Petri Net分析工具对流程进行分析,通过对Petri Net的性质验证来达到对服务流程的验证目的,以在流程定义阶段发现其存在的问题.实际结果表明,采用该工具可以确保服务组合流程设计的正确性,增加服务组合的可靠性.

摘要：Y2002-63279-2 0313037C处理中的标题压缩——一个互联网应用和一个新设计语言=Header compression in handel-c-an Internet ap-plication and a new design language[会,英]/Torkelsson,K.＆ Ditmar,J.//2001 IEEE Symposium on DigitalSystems Design.—2～7(TE)Y2002-63279-62 0313038嵌入式系统设计中的结合语言=Combining languagesin embedded system design[会,英]/Evnst,R.//2001IEEE Symposium on Digital Systems Design.—62(TE)