面向对象的时序逻辑语言

针对时序逻辑语言缺少面向对象概念的现状,对投影时序逻辑进行了扩展,介绍了新的语法和语义。在扩展投影时序逻辑中,基于变量集合的层次化和谓词的分组,给出了对象、类和继承等概念的形式化定义。扩展投影时序逻辑的一个可执行子集被定义为面向对象的时序逻辑语言Framed Tempura++,它能够用于面向对象的程序设计,可以模拟组合Web服务的执行。所给出的实例表明,该语言与Framed Tempura相比,能有效地重用代码,提高了代码的可读性和可维护性。     

进位保留加法器的命题投影时序逻辑组合验证

为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法．该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性．进位保留加法器的验证实例说明了该方法的可行性．     

框架时序逻辑语言MSVL中面向对象机制的实现

针对目前时序逻辑语言存在框架问题、缺少面向对象机制、形式化程度过高等不足,提出了框架时序逻辑语言MSVL,包含新的框架操作符、等待语句和非确定的选择语句等技术,并且能够支持面向对象的程序设计．基于正则形和正则图,给出了MSVL解释器的实现方案．并发访问共享资源的实例表明,MSVL比其他时序逻辑语言更接近高级语言,并且解释器的实现方案是切实可行的．     

投影时序逻辑的公理系统与形式验证

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．     

Verilog程序的命题投影时序逻辑符号模型检测

为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法．依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程序进行验证,从而证明片上系统满足设计规范．以Verilog程序描述的四位同步二进制计数系统的验证实例表明,Verilog程序的命题投影时序逻辑符号模型检测方法是可行的．     

责任政策形式化验证方法

为了验证多Agent系统设计的正确性,将责任政策作为约束多Agent交互行为的高层"需求规格"或"通信协议",对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言,基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法,将政策模型的操作语义定义为Kripke结构的状态迁移系统,政策中Agent行为的约束规则声明为线性时序逻辑公式,使用模型检测器Nu SMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明,该方法可有效分析责任政策的设计缺陷,提高多Agent系统设计的正确性。     

基于有限状态机的指针解引用静态检测方法

为了产生高质量和高可靠性代码,提出一种指针解引用静态检测方法,该方法给出了指针状态转换的有限状态机定义。通过对源代码进行语义分析,得到指针指向信息,建立指针与内存单元之间的映射关系,并根据有限状态机中的指针状态判断指针解引用是否合法。本方法不仅记录了变量的作用域和指针集,还分析了指针的确定指向和可能指向,并对部分控制块采取延迟写入指向的方法,提高了指针解引用分析的精度,同时还可以检测内存释放异常的问题。实验结果表明该方法能有效检测非法指针解引用和内存释放异常。     

自动垃圾回收指针模板类的设计与实现

针对传统指针模型所带来的内存使用上的不便性,设计了新的引用计数指针模型,并给出了引用使用规则.设计了通用的指针模板类,最后给出了测试和结果分析,证明此方法可以解决内存的自动管理问题.     

硬件安全门级细粒度形式化验证方法

针对硬件设计长期缺乏有效的安全验证方法问题,提出了一种硬件安全门级细粒度形式化验证方法．该方法使用形式化语言在逻辑门层面上描述硬件电路的安全属性,构造包含安全属性跟踪逻辑的形式化语义语句,从而将硬件设计转化为电路语义模型,并结合霍尔逻辑三元组理论构造用于验证该模型安全属性的定理．定理的证明过程是以人机交互的方式在定理证明器环境下验证定理的合理性．实验结果表明,该方法能够形式化地遍历电路语义模型的状态空间,精确验证不同输入状态下电路语义模型的安全性．该方法通过构造安全属性跟踪逻辑提高了验证的精确性,结合定理证明提高了验证覆盖率,能够有效地验证硬件设计的安全性．     

融合通信业务门户系统中业务逻辑层的扩展与实现

融合通信业务是提供语音、视频、数据和信息服务的综合业务．该业务提供自助服务门户系统,供集团客户管理员和个人用户对业务进行统一管理,业务门户使用SSH（Spring,Struts,Hibernate）框架搭建系统架构,但传统的基于SSH框架的系统实现方式不能满足该业务丰富的业务需求,因此需要对系统的业务逻辑层进行扩展．本文首先介绍融合通信业务组网环境和自助服务门户系统的功能需求,进而分析该系统对业务逻辑层的区别于其它系统的特殊需求,然后给出了业务逻辑层的扩展方案和具体实现．该业务逻辑层可以与复杂组网环境中的多种设备进行通信,充分发挥了SSH框架的能力．     

应用直角辅助投影法画正轴测图

本文提出了在没有轴测轴的情况下,用直角辅助投影法,根据物体的正投影直接画出其正轴测图。这是画轴测图的一种新方法。随着计算机绘图的应用与发展,该方法必将在更多的方面显示出比用传统的方法画轴测图优越。     

基于时间区间时序逻辑的实时系统统一模型检测

在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质. 为此, 该文使用一个离散时间区间时序逻辑公式建立实时系统模型, 使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质, 在此基础上, 离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题. 该文证明了新方法的有效性以及正确性, 为区间实时逻辑这一类的模型检测问题提供了方法.     

一种改善系统性能的鲁棒H2/D稳定控制方法

利用投影引理得出了控制系统分析和综合的一个新框架.在该框架下针对实多面体不确定连续时间系统,提出了基于扩展LM I条件的鲁棒H2/D稳定的状态反馈控制设计方法,所提出的方法能够使用不同的并且是参数依赖的Lyapunov函数来进行鲁棒控制综合,改善了系统性能且具有较低的保守性,通过仿真进行了验证.     

基于SolidWorks的CAD模型直接切层研究

针对面曝光快速成形系统的需要,提出了基于SolidWorks的CAD模型直接切层方法.利用SolidWorks在工程图环境下的剖切功能,实现对CAD模型的直接切层.解决了对复杂CAD模型切层时出现的截面错位问题.论述了用于多种曝光模式的截面填充样式的实现方法.以该切层方法得到的CAD模型的截面图形作动态掩膜,利用面曝光快速成形系统成功制作出了三维实体原型,表明该直接切层方法适用于面曝光快速成形系统.     

在系统可编程逻辑器件在数字电路实验中的应用

简要介绍了在系统可编程逻辑器件的特点、相应的编程软件， 并结合实例说明了用ＩＳＰＳｙｎａｒｉｏ 软件和ＩＳＰ 数字系统实验板开设数字电路实验的方法。     

基于Pro／ENGINEER的CAD模型直接切层

通过对Pro／ENGINEER的研究,借助其开发工具Pro／TOOLKIT实现了对CAD模型直接切层．切层所得零件剖面图形可直接用于面曝光快速成形系统．该方法与传统的对STL模型文件切层方法相比方便快捷,并且减少了模型表面化引起的零件误差,从而使截面轮廓精度更高．该方法为面曝光快速成形系统快速制作高精度零件提供了基础．     

基于投影寻踪模型的互通式立交选型方法

从统计学角度出发,将投影追踪模型应用到互通式立交选型评价体系中,通过遗传算法来实现互通式立交选型方案的模型求解,描述了该方法应用的关键步骤,并指出对于数据量充分、影响因素明确的准真系统,应用实例表明,采用投影寻踪模型进行方案决策更具有客观性.     

信任谓词的计算语义

讨论逻辑系统中信任谓词的计算语义以及表述信任谓词基本性质的若干公理。首先指出计算的协议组合逻辑在讨论信任关系方面可能存在证明过程与挖掘内在信任关系方面的缺陷;扩展谓词演算系统形成基本协议逻辑并为其添加计算语义以便用于描述安全协议;最后从信任关系的本质含义出发,在基本协议逻辑系统中严格定义信任谓词的计算语义,并通过讨论若干公理反映信任谓词的基本性质。     

可编程控制器在化工过程控制中的应用

通过对某化工系统的过程控制要求分析,阐述了采用可编程序控制器实现化工过程控制的原理,给出了流程图.介绍了化工过程控制系统的信号元件及驱动电器与可编程序控制器的对应I/O接点的地址分配、PLC选型和电气接线.详细介绍了应用逻辑设计法设计可编程序控制器梯形图程序的思想和方法,给出了各个控制步骤的逻辑表达式,编写了实现过程控制的梯形图程序.体现了过程设计思想的一般规律,即：基于工业上的许多过程控制系统都是连续、顺序控制的过程.