面向等价性验证的锁存器匹配算法

为了克服现有等价性验证技术中难以精确匹配锁存器的局限性,提出了一种结合多种方法的新型锁存器匹配算法.该算法结合任意模拟、局部二叉判决图、目标模拟3种方法来匹配锁存器,并使用了类似滤波器的思想,任意模拟对锁存器作初步快速匹配,提出的局部二叉判决图技术降低了发生内存爆炸的可能性,目标模拟则针对性地对锁存器作进一步的划分. ISCAS89电路实验结果表明,该算法与模拟和自动测试矢量生成等方法相比,在运行时间、占用内存和匹配精度等方面均体现出有效性,可用于处理较大规模的时序电路验证问题.     

Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments

Multi-Agent Systems (MASs) have long been modeled through knowledge and social commitments independently. In this paper, we present a new method that merges the two concepts to model and verify MASs in the presence of uncertainty. To express knowledge and social commitments simultaneously in uncertain settings, we define a new multi-modal logic called Probabilistic Computation Tree Logic of Knowledge and Commitments (PCTL^kc in short) which combines two existing probabilistic logics namely, probabilistic logic of knowledge PCTLK and probabilistic logic of commitments PCTLC. To model stochastic MASs, we present a new version of interpreted systems that captures the probabilistic behavior and accounts for the communication between interacting components. Then, we introduce a new probabilistic model checking procedure to check the compliance of target systems against some desirable properties written in PCTL^kc and report the obtained verification results. Our proposed model checking technique is reduction-based and consists in transforming the problem of model checking PCTL^kc into the problem of model checking a well established logic, namely PCTL. So doing provides us with the privilege of re-using the PRISM model checker to implement the proposed model checking approach. Finally, we demonstrate the effectiveness of our approach by presenting a real case study. This framework can be considered as a step forward towards closing the gap of capturing interactions between knowledge and social commitments in stochastic agent-based systems.     

Branching-time logics with path relativisation

We define extensions of the full branching-time temporal logic CTL^? in which the path quantifiers are relativised by formal languages of infinite words, and consider its natural fragments obtained by extending the logics CTL and CTL⁺ in the same way. This yields a small and two-dimensional hierarchy of temporal logics parametrised by the class of languages used for the path restriction on one hand, and the use of temporal operators on the other. We motivate the study of such logics through two application scenarios: in abstraction and refinement they offer more precise means for the exclusion of spurious traces; and they may be useful in software synthesis where decidable logics without the finite model property are required. We study the relative expressive power of these logics as well as the complexities of their satisfiability and model-checking problems.     

程序控制流检测算法优化

暴露在太空辐射环境下的星载计算机,其电子元器件可能因受到高能带电粒子的轰击而造成硬件系统的瞬时故障,所以,需要使用容错技术来提高其可靠性。对一种面向硬件瞬时故障的纯软件控制流检测算法RSCFC(Relationship Signatures for Control Flow Checking)进行了有效的改进,通过对标签S进行分段编码,克服了原算法中存在的待加固程序的基本块总数受机器字长限制的问题,并给出了具体的计算证明。计算结果表明,如果机器字长为64位,那么改进后的算法在设定前提下能单层加固程序的最大基本块数可以超过218。与RSCFC相比,改进后的算法在加固基本块总数比较大的程序时,性能开销明显降低而且检错能力保持不变。     

基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁

形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于 Promela 语言,将 P ．Maggi 和 R ．Sisto 提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam 协议为例,运用 Spin 工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。     

RCC高速缓存一致性协议的带参验证

Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统,对此协议的带参验证是一个很大的挑战。 Cubicle是最近出现的基于SMT求解器的带参模型检测工具。我们使用了Cubicle带参模型检测工具,成功对RCC协议进行了建模和验证。实验结果表明, RCC协议在结点个数为任意规模时均满足协议的各种安全性质。     

带时间和资源约束的实例化过程模型验证方法

软件过程的性能是由软件过程模型和软件过程实例化两方面因素决定,如果对软件过程进行了不恰当的实例化,会导致成本超支、进度延期、甚至项目失败．已有的过程描述法不足以分析实例化过程模型,由于没有考虑实例化阶段的时间资源约束,语法结构正确的过程模型并不能保证过程执行的正确性．提出一种带时间和资源约束的实例化过程模型验证方法,为目前已有的s-TRISO／ML建模语言增加时间和资源约束属性,然后提出了从s-TRISO／ML模型转换成时间自动机的转换方法和实现算法,利用已有的分析工具Uppaal对转换得到的时间自动机的性质进行验证,得到一个合理的实例化模型,从而为真实的开发流程提供指导．     

一种可扩展的动态数据持有性证明方案

提出了一种能保护数据隐私的动态数据持有性证明方案, 并对方案的安全性进行了证明, 性能分析表明该方案具有低存储、计算和传输负载的特点。通过扩展实现了对公开可验证和多副本检查的支持, 扩展方案的特点在于公开验证中不需要可信第三方的参与, 而多副本检查可以方便地实现对所有副本的批量检查。     

基本主方向关系的反关系推理

在深入研究了基于MBR的主方向关系的反关系推理的基础上,提出了一种基于区域对象本身的基本主方向关系的反关系推理算法。在理论上对该算法的正确性和完备性进行了证明,并通过与实际情形逐一对比验证了该算法的正确性。     

基于模型检测的工作流访问控制策略验证*

访问控制策略的有效性对工作流管理系统的安全稳定运行具有重要影响,针对这一问题,提出了一种基于模型检测的工作流管理系统访问控制策略验证方法。建立了工作流管理系统的访问控制策略模型与工作流执行主体任务权限状态模型,并在此基础上对访问控制策略的有效性进行验证。实验表明该算法具有有效性和合理性,为访问控制策略的验证提供了一条新的解决途径。