逻辑未知PLD的安全性漏洞检测方法

针对逻辑未知PLD的孤立状态检测,对黑箱检测法进行研究。通过分析PLD的I/O结构,阐述检测过程中引脚属性判别的原理,对比分析3类判别算法的性能。针对状态驱动问题,阐明现有驱动算法的实现思想,分析现有驱动算法的空间复杂度,并且针对状态搜索和转移路径长度,定性地分析时间复杂度,提出下一步研究的重点。     

基于ASP.NET与Amzi! Prolog混合编程开发专家系统的研究

针对ASP.NET网站开发中可能遇到的逻辑推理问题,提出并实现了用Prolog语言与ASP.NET混合编程方法开发专家系统框架的方案,为开发基于Web的专家系统提供了一条方便快捷和高效的途径。此方案用ASP.NET2.0(C#)实现专家系统的Web用户界面,用Prolog语言实现推理过程,介绍了该专家系统的实现原理,给出了关键程序连接语句用来论述其结合技术,从而提高了软件开发的效率。     

From Flow Logic to static type systems for coordination languages

Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language Klaim.     

Fast computation of the prime implicants by exact direct-cover algorithm based on the new partial ordering operation rule

In this study, a novel OFF-set based direct-cover Exact Minimization Algorithm (EMA) is proposed for single-output Boolean functions represented in a sum-of-products form. To obtain the complete set of prime implicants covering the given Target Minterm (ON-minterm), the proposed method uses OFF-cubes (OFF-minterms) expanded by this Target Minterm. The amount of temporary results produced by this method does not exceed the size of the OFF-set. In order to achieve the goal of this study, which is to make faster computations, logic operations were used instead of the standard operations. Expansion OFF-cubes, commutative absorption operations and intersection operations are realized by logic operations for fast computation. The proposed minimization method is tested on several classes of benchmarks and then compared with the ESPRESSO algorithm. The results show that the proposed algorithm obtains more accurate and faster results than ESPRESSO does.     

基于TLA的UML模型形式化验证

统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为 2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。     

基于Simulink／Stateflow的汽车防抱死系统的建模与仿真

防抱死系统（即ABS）是汽车关键的安全装置之一。该文在Simulink／Stateflow的环境下对ABS进行建模,用逻辑门限控制算法来建立控制模型,并对所建立的汽车制动系统模型进行仿真,得到仿真曲线,以验证汽车在不同路面上行驶时的制动性能。     

基于FPGA的逻辑分析仪连续触发模块设计

该文介绍一种逻辑分析仪数据捕获模式的设计原理与实现方法。该模式主要用于嵌入式软件的测试分析,它不再采用采样的方式来采集数据,而是利用软件插桩与硬件设置触发字相结合的方法来监视系统总线。当程序运行到插桩点时,硬件将产生触发,此时才会主动地到总线上将相应数据与对应的具体时问捕获回来,从而实现有效数据的精确捕获。此外,在FPGA内部采用双RAM交替读写的方式来暂存数据,在不中断程序运行的情况下,实现有效数据的长时间实时存取与分析,提高嵌入式软件性能分析的范围和质量。采用FPGA作为构成硬件架构的基本功能器件,提高了工作速度,使整个设计具具有集成度高、性能稳定、调试方便等特点。该模块在实际应用中得到了验证,并取得了良好的效果。     

The Shadow Knows: Refinement and security in sequential programs

Stepwise refinement is a crucial conceptual tool for system development, encouraging program construction via a number of separate correctness-preserving stages which ideally can be understood in isolation. A crucial conceptual component of security is an adversary’s ignorance of concealed information. We suggest a novel method of combining these two ideas.Our suggestion is based on a mathematical definition of “ignorance-preserving” refinement that extends classical refinement by limiting an adversary’s access to concealed information: moving from specification to implementation should never increase that access. The novelty is the way we achieve this in the context of sequential programs.Specifically we give an operational model (and detailed justification for it), a basic sequential programming language and its operational semantics in that model, a “logic of ignorance” interpreted over the same model, then a program-logical semantics bringing those together — and finally we use the logic to establish, via refinement, the correctness of a real (though small) protocol: Rivest’s Oblivious Transfer. A previous report^? treated Chaum’s Dining Cryptographers similarly.In passing we solve the Refinement Paradox for sequential programs.     

Plans, Actions and Dialogues Using Linear Logic

We describe how Intuitionistic Linear Logic can be used to provide a unified logical account for agents to find and execute plans. This account supports the modelling of agent interaction, including dialogue; allows agents to be robust to unexpected events and failures; and supports significant reuse of agent specifications. The framework has been implemented and several case studies have been considered. Further applications include human–computer interfaces as well as agent interaction in the semantic web.