基于逻辑工作流网的有限无死锁组合

以逻辑工作流网作为描述过程模型的方法,提出了逻辑工作流网的有限组合,以状态转换图来描述工作流网的可达逻辑活动序列。根据死锁的充分条件,提出状态映射用以判断两个工作流网组合后出现的死锁。通过删除进入死锁的逻辑活动序列,提出标准伙伴状态转换图用以表述无死锁组合的活动序列。最后提出判断有限组合是否存在死锁的方法,并用一个简单的电子商务实例说明了方法的有效性。     

一种验证Web应用设计的方法

提出一种表示Web应用的请求/响应导航关系的形式化行为模型,给出一种基于模型检查的Web应用设计的验证方法并描述了用时态逻辑CTL表示Web应用性质的方法.设计了一个检验方法可行性的原型框架,该原型嵌入自动化模型检查工具NuSMV,提供从UML设计模型到形式化模型的自动转换,在将用户输入的性质和形式化模型合并为NuSMV程序后,运行NuSMV进行自动化验证.     

解开计算机硬盘死锁的一种方法

本文介绍硬盘逻辑死锁的原因，并给出了解开硬盘死锁的思路和详细的程序。     

计算机辅助气动系统逻辑设计的研究

对计算机辅助气动系统逻辑设计进行了深入研究，选择逻辑综合的方法作为计算机辅助气动系统逻辑设计的基础理论基本方法，采用立方符号表述逻辑函数，把逻辑运算表示为立方的相交、相容及锐积运算，提出用判断最小项来完成对给定程序的判和校正，进而实现了计算机辅助逻辑综合，得到了的逻辑设计结果。     

直觉模糊逻辑中的归结原理

在模糊逻辑归结原理的基础上，用（０，１）中的两个实数表示一个命题“真的程度”和“假的程度”，从而提出了直觉模糊逻辑，本文提出直觉模糊逻辑的归结原理，并证明其完备性。     

用电子计算机辅助简化逻辑函数

本文根据正三角形桁架图形构成原理,提出了编制用计算机辅助多变量逻辑函数简化通用程序的方法。如果根据这种方法编制一个n变量通用程序,它不仅适用于n变量各种逻辑函数,也适用于n变量以下各种逻辑函数。对于变量数超过n的各种逻辑函数,只要它们的标准项的等效十进数最大不超过(2~n-1),这个通用程序也能适用。     

UML 顺序图的一种形式化描述方法

统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。     

基于Petri网的知识表示

介绍一种基于Ｐｅｔｒｉ网的知识表示方法。在引入Ｐｅｔｒｉ网的基本知识后，详细讨论了Ｐｅｔｒｉ网表示产生式系统及基于Ｈｏｒｎ逻辑子句的Ｐｅｔｒｉ网表示，提出了用库所表示产生式谓词，用变迁表示规则的Ｐｅｔｒｉ模型。最后讨论了将Ｐｅｔｒｉ网应用于ＯＯＡ（面向对象分析）模型的研究，从而提出一个基于Ｐｅｔｒｉ网的ＯＯＡ模型     

扩展颜色逻辑Petri网及其可达性分析

逻辑Petri网是一种增广Petri网模型,具有与图灵机等价的建模能力。颜色逻辑Petri网解决了逻辑Petri网中输出的不确定性表达问题。然而颜色逻辑Petri网描述不同子系统的并发过程,需要对每一个子系统建立一个子网模型。如果所有子网模型的结构相同,则可以引入多个有色托肯,从而用一个子网模型表示多个子系统的并发过程。因此,提出了扩展颜色逻辑Petri网模型及其可达性分析方法。首先,为了方便可达标识的表示和计算,引入多重集的素数表示法,用素数幂的乘积来表示一个多重集,并给出了判断变迁使能的方法。其次,通过定义颜色逻辑关联矩阵,给出了一步可达标识的计算公式以及可达树构造方法。最后,针对一个电子商务实例,分别用颜色逻辑Petri网和所提出的扩展颜色逻辑Petri网建立模型并进行比较分析,从而证明了提出的模型具有更简单的网结构,丰富了逻辑Petri网理论。     

单向通信保密系统的时序逻辑验证

探讨了形式化验证加密协议的方法，用时序逻辑验证了单向保密协议的安全性缺陷。     

分离逻辑的技术基础与研究现状

随着计算机系统复杂性的日渐增加,可靠性正成为计算机软件理论中新的研究热点.运用数理逻辑中的推理方法,研究人员可以严格分析和验证计算机程序的正确性.分离逻辑作为一种分析共享可操作存储程序的新方法,近年来逐渐发展成为针对可扩展程序的主流验证技术之一.文章阐述分离逻辑的研究背景、理论基础以及验证原理,详细介绍其对存储空间抽象描述的思想,通过实例说明分离逻辑的推导策略.特别地,介绍了双向诱导推理对循环链表程序片段的验证过程,展现了在未知系统当前状态的情况下,分离逻辑验证未完成代码,甚至代码片段正确性的可行性.文章还综述了诸多基于分离逻辑的各种拓展,以增加对分离逻辑研究状况的了解.     

用逻辑代数设计PC程序

通过介绍用逻辑代数设计ＰＣ程序，使控制机床运行的程序变得更为简洁一些，在实际的设计过程中应用了这种技巧，取得了良好的效果。     

基于时态逻辑语言XYZ／E的软件体系结构研究（Ⅰ）－－基本组件和连接件的描述

XYZ／E是世界上第一个可执行的时态逻辑语言，它既能描述抽象静态语义，又表表示程序的动态语义，这一特征恰好分层描述软件体系结构。本文采用XYZ／E语言刻画了软件体系结构的基本组件与连接件；它为进一步描述体系结构风格提供了一个基础。     

程序设计的一种逻辑分析方法

针对程序设计中逻辑分析不清晰、不简洁、不严谨，致使程序冗长复杂、质量不高的情况，提出利用数字电路设计中的逻辑分析工具——卡诺图，先对逻辑关系进行分析化简，再进行编码的程序设计方法，提出一种把浅显的思维判断，转变为深刻的数学分析的程序设计思路，同时，结合典型实例，阐述了这种方法、思路的使用步骤。     

基于规约说明语言的面向对象软件测试

提出了一种测试面向对象程序的框架模型．用Object-Z语言描述面向对象程序的形式化规约．从形式化规约说明中可以推导出的面向对象程序的状态转换图，状态图可以表示面向对象程序的动态行为，并且可以用来描述一个由面向对象程序的方法调用序列组成的测试数据集．最后给出了验证一个方法调用序列正确性的方法．测试结果显示这一框架模型对于测试面向对象程序是可行的．     

用分层ATMS实现缺省逻辑

Ｒｅｌｉｅｒ的缺省逻辑存在着局限性．它无法表示缺省规则之间的优先级，无法处理缺省规则中析取，并且不满足累积性．虽然Ｂｒｅｗｋａ提出带优先级的缺省逻辑和累积缺省逻辑，但不能完全克服上述局限性．本文介绍了分层ＡＴＭＳ，然后指出用分层ＡＴＭＳ实现的缺省逻辑能克服现有缺省逻辑中的局限性．     

基于时态逻辑语言XYZ／E的软件体系结构（Ⅱ）——常见体系结构风格的描述

XYZ／E是世界上第一个可执行的时态逻辑语言，它既能描述抽象静态语义，又能表示程序的动态语义，这一特征恰好适合分层描述软件体系结构，文[1]采用XYZ／E语言刻画了软件体系结构的基本组件与连接件。本文讨论如何通过对这些组件及连接件进行特定的组合，来表示几种重要的软件体系结构风格。     

VLSI综合的逻辑最小化算法

本文讨论了逻辑函数的多维体空间表示方法和运算方法，探讨了接近量小覆盖的两级与－或网络的自动逻辑综合方法，提出不经过求出全部质蕴涵项而直接构成函数的无冗余覆盖的算法，该算法主要用于可编逻辑阵列（ＰＬＡ）及与－或网络的自动综合。     

通用阵列逻辑GAL器编程方法的研究

介绍了通用阵列逻辑ＧＡＬ器件的输出逻辑宏单元结构及组态模式，重点就ＧＡＬ器件编程中选择输出方式，合理分配引脚处理相邻性问题，选择逻辑问题的描述方式以及ＡＢＥＬ软件编辑中的几个技术问题进行了分析与探讨。     

UNITY逻辑中关于unless的若干结果

本文的工作主要分为两部分．首先，我们把验证ｐｕｎｌｅｓｓｑ是否是ＵＮＩＴＹ逻辑的定理转化为一阶定理的验证．其次，设ｐ１ｕｎｌｅｓｓｑ１，…，ｐｎｕｎｌｅｓｓｑｎ在一ＵＮＩＴＹ程序Ｆ中成立．我们把验证ｐｕｎｌｅｓｑ在Ｆ中成立是否可由以上ｎ个性质得出转化为强推出的验证，其中强推出是本文引进的新概念．