时序电路的形式化证明

对硬件的形式化验证是硬件验证的一个发展方向,形式化验证一个时序电路就是证明电路的实现是否满足他的规格描述.本文提出了用等式逻辑ε的一个公式Ws来表示电路的实现,用Tempura的程序B表示对该电路的特性描述.公式B（∈）P引入来证明电路的正确性,这里P是电路的初始状态,是从Ws中抽取的,另外还要从Ws提取输出等式.这样,一旦证明了B（∈）P,就能证明实现满足规格描述.最后,给出了一个例子来说明此证明方法.     

微内核架构内存管理的形式化设计和验证方法研究

由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS（Verified Secure Operating System）内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.     

UML状态机到B形式化规约的转换

文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点．将其转换为B形式化模型，然后在B工具环境中遵循B方法的精化原则和正确性验证方法，开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则，涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明．这套转换规则行之有效。     

网络协议描述及正确性证明方法初探

本文先以几个例子为基础浅谈了网络协议的自然语言描述和形式化描述,然后讨论协议正确性的证明方法,并对各种方法作了简单比较。     

基于并发事务逻辑的Web服务编制验证

 服务编制解决的是组织之间的业务集成问题,面临的是一个广泛分布、动态、自治、异构的网络环境,保障组合服务的正确执行以及相关特性的验证问题显得尤为重要.形式化方法是一种有效的解决方法,服务编制需要建立在严格的形式化模型的基础上,可以通过具有明确的、形式化语义的形式化模型研制验证工具来完成组合服务正确性的验证.本文基于并发事务逻辑(CTR:Concurrent TRansaction Logic)对服务编制的元素进行了描述和建模,给出了从WS-BPEL到并发事务逻辑的转换规则,讨论了服务编制在CTR中的验证问题以及WS-BPEL和CTR的表达能力,最后给出了一个实际的服务编制在CTR中建模的例子,验证了服务编制的CTR模型的有效性.     

SIP协议系统模型的形式化研究

通信协议形式化是提高其可靠性和正确性的重要手段.会话初始协议SIP是软交换的一个主要协议,应用形式化方法研究了SIP协议的结构及系统模型,主要从系统级和功能级上使用形式化规格描述语言SDL和消息顺序图MSC对SIP协议主要系统组件进行形式化描述,得到了SIP协议的形式化规范,并应用形式化方法进行了验证.为SIP协议部件库研究开发提供形式化技术基础.     

拟态路由器BGP代理的设计实现与形式化验证

为确保拟态路由器中协议代理等“拟态括号”关键组件的安全性和功能正确性，设计实现了边界网关协议（BGP）代理，并采用形式化方法对BGP代理的安全性和功能正确性进行了验证。BGP代理通过监听邻居路由器与主执行体之间的BGP会话报文，模拟邻居路由器与从执行体展开BGP会话，实现各执行体的BGP状态一致。采用VeriFast定理证明器，编写基于分离逻辑的形式化规约，证明程序不会出现空指针引用等内存安全问题，并验证了BGP代理各功能模块实现的高级属性符合功能规约。BGP代理实现与验证代码量之比约为1.8:1，程序设计实现和程序验证所耗费的时间之比约为1:3。经过形式化验证的BGP代理处理100 000条BGP路由所花费的时间为0.16 s，约为未经过验证的BGP代理的7倍。研究工作为应用形式化方法证明拟态防御设备与系统中关键组件的安全性和功能正确性提供了参考。     

基于uppaal的电压型配电自动化建模与仿真

由于传统方法对电压型配电自动化的动作过程的分析缺乏严格的数学定义与模型验证,导致结论保守或者不完备。为了解决这个问题,使用模型检测的方法实现对其动作过程的分析,提出一个用于电压型配电自动化的分析模板,通过时间自动机理论建立形式化模型,并使用模型工具uppaal对其动作过程建模与性质验证。仿真结果能够验证所述模型的活性、正确性和平滑性。通过对模型的科学验证,证明电压型配电自动化在配网自动化建设上具有重要意义。     

一种面向瞬时故障的容错技术的形式化方法

软件发生瞬时故障时,可能会导致处理器状态改变,致使程序执行出现数据错误或者控制流错误.目前已有许多软件、硬件以及混合的解决方案,主要的方法是重复计算和检查副本的一致性.但是,生成正确的容错代码十分困难,而且几乎没有关于证明这些技术的正确性的研究.类型化汇编语言(TAL)是一种标准的程序安全性证明的方式.本文概述了一种面向瞬时故障的软硬结合的容错方法,以及对该方法的形式化方法,包括容错类型化汇编语言、类型系统和容错定理.形式化的目的是为了验证,只有通过验证的程序代码才是类型安全的.本文只简单介绍了程序的形式化方法.     

基于抽象状态机的普适服务组合分析与验证

提出了一个普适环境下服务组合的框架,使用抽象状态机对服务的行为进行不同精化层级的形式化描述,然后利用 CoreASM 这一模型检测工具对服务组合进行模拟执行验证,从而验证服务组合的正确性.最后给出了一个运用此方法进行服务组合验证的典型应用场景.     

基于B方法的电梯控制系统形式化研究

B方法是一种新的形式化方法,使用B方法开发软件可有效提高软件的可靠性、可复用性和开发效率.文中使用B方法对电梯控制系统建立了抽象机模型并对其进行活性证明,自动生成相应软件,提高了电梯控制系统的可靠性和稳定性.     

软件形式化开发方法的选择策略研究

随着软件形式化方法的不断发展,各种各具特色的形式化方法涌现出来,为了解决在具体的系统开发中如何选取合适的形式化方法,对目前较为流行的几种形式化方法RSL,B,VDM,Z的特点进行对比分析,然后针对不同的软件开发人员和所需开发系统的不同,给出了适合用形式化方法开发的情况和如何选择合适的形式化开发方法。     

非屏蔽多芯线缆耦合通道大电流注入等效试验方法

从非屏蔽多芯线缆单一线对大电流注入等效替代辐照模型出发,提出了单一线对的大电流注入严格等效辐照的试验方法.以非屏蔽四芯线为试验对象,探索了非屏蔽多芯线缆终端响应规律,发现各线对并不能同时严格等效.在此基础上,提出了非屏蔽线缆耦合通道加严等效的试验方法,并进行了试验验证.试验结果证明,提出的大电流加严等效注入的方法是可以...     

扩展的模糊时间Petri网

网络实时系统对时间和QoS有严格要求.扩展的模糊时间Petri网是一种对网络实时系统进行建模和分析的形式化模型,Petri网数学理论基础能保证并发系统的可靠性和正确性.本文介绍了扩展的模糊时间Petri网的定义,模型检验方法,仿真工具,网精简技术和应用领域,并探讨了进一步研究的方向.     

片上系统的模型检验

片上系统(SoC)的验证是一个比较复杂的问题，仅靠模拟仿真无法保证SoC设计的正确。形式化方法是利用数学推理的方法来证明其正确．是对SoC设计进行验证的一条重要途径。模型检验技术是一种完全自动化的形式化方法，针对模型检验技术，讨论了在SoC验证中的应用，指出在SoC设计中，只有把模拟仿真与形式化、半形式化的方法结合起来，才能更好的对SoC进行验证。     

某C~3I系统指挥与通信能力检测方案与思考

某C3I系统在研制和生产中,使用了模拟测试平台的方法对其指挥与控制功能进行了测试、检验及验收;由于测试方法逼近实装测试条件,所以测试结果直观、容易和战技指标相对应。其模拟测试平台的设计和制造并不需要较高水平的人员就可完成。但由于模拟检测平台庞大,构建经费很高,造成维护困难,鉴定繁琐,希望能探索其他类似仿真测试平台的方法开展此项工作。     

论有限回溯测试模式产生方法

本文首先剖析了有限回溯测试模式产生(FBTPG)方法的实质,然后在深入分析三种ATPG系统的C-B曲线的实验数据的基础上,提出故障模拟对测试生成的综合调节效应,为FBTPG方法的有效性提供了理论依据.最后以ISCAS-85和ISCAS-89电路为基础,给出了FBTPG与随机测试生成、确定性测试生成和商用ATPG系统FlexTest的实验比较结果,从而论证了FBTPG方法处理超大规模时序电路的有效性.     

On Formal Modeling and Validation of Wireless Sensor Network Protocols

Formal verification is becoming more and more important in the field of wireless networks (WSN). The general purpose formal method called Event-B is the latest incarnation of the B Method: it is a proof based approach with a formal notation and refinement technique for modeling and verifying systems. Refinement enables implementation level features to be proven correct with respect to an abstract specification of the system. This paper proposes an initial attempt to model and verify consistency and correctness of a WSN operation in its different layers. Several formal models are introduced for this type of networks. In the first time, coloured Petri net are used to elaborate network layer models, then each one will be detailed by an Event-B formalism, while proofs are carried out using the RODIN platform which is an integrated development framework for Event-B.

     

基于XML结构的C语言考试的自动评分系统

在C程序设计语言考试中为了解决定位难、一题多解和对于主观题没有统一的评价标准的情况,对考试系统中客观题和程序题的评分方法进行了研究。在比较结果的评分基础上,引入了XML结构的答案库,以及使用了黑盒测试方法与抽取骨架的方法,成功地解决了上述问题。在设计系统的过程中,十分注重软件的实用性。该系统设计成功后,通过在小范围内使用,初步实验结果证明自动评分模块运行稳定,评分标准能够统一。