O-表达式的性质定义与规范（英文）

在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式。给出了此类表达式（O-表达式）的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式。具有明确运行目标的O-表达式称为独立O-表达式（stand-alone O-expression,saloe）。一个完整的程序可能由若干个saloe组成。给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。     

Arnold反变换的规范表达式及多维推广

Arnold变换具有周期性,广泛应用于图像加密方面,其正变换具有规范的表达式,但Arnold的反变换却没有一个规范表达式,因此论文提出一种Arnold反变换的规范表达式对各类Arnold正反变换进行形式上的统一,规整而简洁化,并在多维上进行推广。     

表达式的检错与计算

在各种计算机语言和许多应用系统的命令中,都包含有表达式,而这些表达式是怎样被识别和处理的呢? 本文介绍的程序,将把键盘输入的一个由运算数,运算符(+、     

表达式与二叉树的相互转换

数学表达式、栈的操作、二又树的遍历,这几个概念在数据结构的教材中是不可缺少的。数学表达式求值是程序设计语言编译中的一个最基本问题,也是栈应用的一个典型例子,用它来研制出各种类型的电子计算器（前缀计算器、中缀计算器（常见的计算器）、后缀计算器）。在数据结构中没有解决表达式与二又树之间的相互转换关系,也就是说不能由一种表达式迅速地得到另外的两种表达式,也就难于解决其他两种计算器的研制过程。本文旨在研究表达式与二叉树间的相互转换关系,便于由一种表达式（或表达式树）迅速求出其他的表达式,再通过栈的应用（操作）研制出三种不同的计算器（栈的应用在数据结构的教材中都有,在此文中不予介绍）。     

Petri网的进程表达式与语言表达式

Petri网的语言和进程都是网系统行为的一种有效的描述手段,对应的进程表达式和语言表达式给出了系统全体行为的约束描述．本文首先对Petrl网的进程表达式进行了类型的划分并给出了相应的代数判定依据，随后证明了Petri网的进程表达式与语言表达式的类型一致性，由此给出了由进程表达式求取语言表达式的算法，为基于Petri网语言(尤其是无界Petri网)分析实际的物理系统提供了更为有效的途径．     

路径表达式的并行算法研究

在面向对象数据库系统中,路径表达式是用于定位复杂对象的必要查询设施,因此,优化和并行化路径表达式的执行是实现高性能面向对象数据库系统的关键因素之一,由于ＯＱＬ语言的正交性,在ＳＥＬＥＣＴ,ＦＲＯＭ和（或）ＷＨＥＲＥ子句中均可嵌套路径表达式,而我们将着重讨论ＷＨＥＲＥ子句子路径表达式的并行计算,种路径表达式也称之为复杂谓词。本文分析了现有路径表达式的计算方法后,提出了两种新的路径表达式并行计算算法,     

逻辑函数表达式的化简

在设计制作数字电路时,经常要化简逻辑函数表达式,本文介绍了化简逻辑函数表达式的方法,重点讲解了应用卡诺图方法化简表达式的技巧。     

数学表达式的实时输出

用 VB实现了数学表达式在应用程序中的实时输出。对其实现方法、主要程序块及其优缺点作了较详细的阐述。     

使用递归下降算法分析数学表达式

本文介绍使用编译原理理论中的LL(1)算法中最简单的种形式-递归下降算法来解决数学表达式的解析问题。同时．也介绍手工构造EBNF文法的分析器代码的方法．本文能对开发自己的语法分析器带来帮助。     

Word文档中数学表达式的编辑方法

介绍Word中数学表达式的编辑方法和步骤.     

基于动态分析的软件不变量综合技术

软件不变量是软件的重要属性,在软件验证、软件调试和软件测试等领域有重要作用.自20世纪末以来,基于动态分析的不变量综合技术成为相关领域的一个研究热点,并且取得了一定的进展.收集了90篇相关论文对该领域进行系统总结.基于动态分析的不变量综合技术是该领域的核心问题,提出了"学习者-预言"框架统一描述相关方法,并且在此框架内根据学习者的归纳方法将综合技术大致分为4类,分别是基于模板穷举的方法、基于数值计算的方法、基于统计学习的方法以及基于符号执行的方法.其次,讨论了基于动态分析综合的不变量在软件验证和软件工程等领域的重要应用.随后,总结不变量生成技术中常用的实验对象程序和开源的不变量综合工具.最后,总结该领域并展望未来的研究方向.     

覆盖率驱动的芯片功能验证设计与实现

随着芯片集成度的发展,芯片性能越来越高,而上市时间越来越短,芯片验证在芯片设计中非常关键并贯穿于整个设计过程,验证的效率和质量直接决定着芯片的成败。提出了基于覆盖率驱动的芯片功能验证方法,定义了基于功能点覆盖率驱动的验证流程,利用PSL语言描述断言检查很有效,通过模拟工具检查断言是否成功,从而判断设计是否满足系统的功能要求。在网络接口芯片实际应用中,有效地降低了验证工作的复杂度,同时提高了验证的速度和质量。利用功能覆盖率数据判断测试激励的正确性和完整性,同时用覆盖率数据定量评价验证进程,提高了整个设计的效率。     

PSL逻辑及验证技术研究进展与展望*

在简要介绍PSL的分层结构和语法与语义基础上,综述了PSL验证技术的应用研究现状,分析了各种方法、技术的优缺点,最后指出了PSL验证技术的未来研究展望。     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

Prospec: Support for Elicitation and Formal Specification of Software Properties

Although formal verification techniques have been demonstrated to improve program dependability, software practitioners have not widely adopted them. One reason often cited is the difficulty in writing formal specifications. This paper introduces Prospec, a tool to assist practitioners in formally specifying software properties. Prospec uses property patterns and scopes. Previous efforts at providing tool support for property specification have not provided convenient abstractions for specifying properties that include multiple events or conditions. A taxonomy of composite propositions is introduced to address this issue by defining relations among propositions and providing graphical abstractions that can assist in specification and validation of properties. This paper shows how composite propositions can enhance the specification pattern system by helping practitioners consider subtleties of behavior in sequences and concurrency through directed questions and visual abstractions. The paper introduces an elicitation and specification process to define patterns, scopes, and composite propositions.     

基于PSL断言的宽带电路交换芯片验证

利用基于PSL断言的验证方法验证了宽带电路交换芯片XYDXC160的设计。该芯片单片支持64路2.488Gb/s STM-16帧结构的SDH码流的输入/输出，实现1 024×1 024 STM-1流的无阻塞电路交换。断言技术的引入，降低了验证工作的复杂度，提高了验证的速度和效率，确保了验证工作的质量。     

Demonstrating the Cognitive Plausibility of Interactive System Specifications

Much of the behaviour of an interactive system is determined by its user population. This paper describes how assumptions about the user can be brought into system models in order to reason about their behaviour. We describe a system model containing reasonable assumptions about the user as being ‘cognitively plausible’. Before asserting the plausibility of a model however we must first be able to make the assumptions made in that model inspectable. There is a tension between the inspectability of user assumptions and the tractability of models; inspectable models tend to not be very tractable and vice versa. We describe how we can get round this tension, by deriving tractable models from explicit user assumptions. The resulting models may not of themselves be very inspectable to human-factors workers, but the process by which they are derived is inspectable. Hence we claim that we can have both tractability and inspectability. We exemplify our claims using a simple cognitive model and ‘Meeting Maker’, an interactive electronic diary system. Received March 2000 / Accepted in revised form July 2000     

基于分离指标的宽阻带低通滤波器设计

常见的开路短截线和阶跃阻抗结构在微带低通器设计中较为成熟,但是这些结构的低通滤波器受到寄生通带的影响,阻带不够宽;提出了一种基于分离指标的宽阻带低通滤波器设计方法,利用计算机仿真软件ADS,对常见的阶跃阻抗低通滤波器进行结构改进;该方法将低通滤波器设计指标重点分为滚降率和宽阻带抑制两部分,分别利用椭圆滤波器和巴特沃斯滤波器的本身特性实现设计目的,最后进行级联优化;此结构综合设计方法简单严谨,易于实现,改进的低通滤波器性能优越,实现了宽阻带的设计需求,通带0~3 GHz,插入损耗<0.5 dB,阻带4~12 GHz,抑制>45 dB。     

基于接收信号强度的非视距检测与修正算法

为了减少非视距（NLOS）误差对基于到达时间（TOA）的无线定位系统性能的影响,本文提出一种采用接收信号强度（RSS）与TOA测量值相结合的方法对含有NLOS误差的TOA测量值进行检测并修正。在视距（LOS）传播的TOA与RSS之间关系已知的前提下,利用定位基站得到的TOA与RSS测量值,计算TOA测量值中含有NLOS误差的可能性,并利用该可能性对TOA测量值进行修正。该方法在不增加通信次数的情况下,大大提高了定位精度。本文最后在一个无线定位系统上实现了该算法,并进行了对比实验。实验结果表明,该算法不需对多次定位结果进行统计,即可有效降低NLOS误差对系统性能的影响,适用于对功耗要求苛刻的场合。