模型检测中的偏序约简

检查并发系统的性质变得日益困难。随着验证方法的发展,一些复杂系统并发性越来越高,越来越难以理解。偏序约简方法被提出以减少自动验证并发系统所需要的时间和内存。文中介绍了偏序约简技术的主要概念和基本算法,介绍了其在LTL中的应用,提出了改进方法。     

基于Petri网的CSP并发系统验证技术研究

通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。     

基于SPIN／Promela的并发系统验证

并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一，其成功应用归功于有效验证工具的支持。SPIN是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述SPIN工作机理的基础上，详细分析了基于SPIN的系统建模语言Promela中通道操作、基本数据结构及其功能，并设计了SPIN形式化验证软件系统的基本算法，最后运用SPIN对一个并发系统实例进行验证，得出了相应验证输出图。     

并发行为推理的一种进程代数方法

在人工智能领域，动态系统的行为推理是一个非常热门的研究课题，其中最重要的问题是如何描述系统以及如何进行推理。在这一方面，人们已经提出很多形式化的方法。典型的描述动态系统的方法是引进一个取值随系统进化而改变的“事实”(fact)的集合，以及定义行为对“事实”的影响函数，以方便描述由执行特定的动作引起的状态转移；典型的推理问题是逻辑蕴涵，即寻找一种特定的适合描述动态系统的逻辑，在此逻辑下，系统状态的属性可以由有关系统的一些假设出发推导出来。     

基于Petri网的分布式系统并发进程的死锁检测

分布式系统中的并发进程具有明显的并发、异步及分布性,而Petri网是模拟与分析并发、异步、分布式系统的有效工具.为此通过引入Petri网,给出了分布式系统局部并发进程等待的Petri网模型及死锁检测方法,提出了全链路合成的概念,利用全链路合成技术组装了全局并发进程等待的Petri网模型,给出了判断整个系统是否出现死锁的充分必要条件.     

基于进程代数EACSR-VP的通信模型的实现

介绍了进程代数EACSR—VP的基本通信原语,详细阐述了并发系统中通信模型的建立与实现,并给出了分析与讨论。     

基于FSP的安全性与活动性检测技术

安全性与活动性是并发系统和分布式系统的两类基本性质,快速检测安全性与活动性在这类系统的设计和开发过程中具有重要的实际意义。本文给出基于FSP进行安全性与活动性检测的方法并给出具体的实例分析。     

具有动作细化的实时并发进程的基于事件的操作语义以及一致性结果

对于包含动作精化的实时进程代数，人们已经为它定义了指称真并发语义。在这种语义里，动作精化被看作是一个操作符。人们自然会有这样的疑问：既然已经定义了指称真并发语义，为什么还要定义操作语义?这个问题可以从以下两个方面回答：首先，对于不带时间变量和动作精化操作的进程，为它赋予一个“标准”语义的含义就是指为它定义一个操作语义。定义操作语义常用的方法是定义一个具有标记的传递系统，它是由一些推理规则组成的集合，这些推理规则刻画了实际程序或系统     

基于偏序关系的演化算法

在演化算法中引起卢偏序关系（称为优适应关系）,把评估个体适应性能的机制从适应值函数一般化为优适应关系,在此基础上定义演化算法求解的问题一般形式并修正了演化算法的基本结构,从而使演化算法概念更清晰,在理论上澄清了一些演化算法概念上的分歧,为演化算法应用于更广泛的领域提供理论指导。     

基于偏序归约的状态空间约简算法

目前,针对安全协议分析的偏序归约算法较为复杂且不易实现,限制了其适用范围,未考虑约简诚实主体会话中的逆序结点。针对该问题,采用偏序归约的思想,提出一种诚实主体会话中逆序结点的约简算法以及一种迹等价迁移冗余后继结点的约简算法。两种算法思想简单,易于实现。实例表明,这两种算法有效地约简了安全协议的状态空间。     

基于远程帧缓冲的多路并发技术支持系统

针对气象业务通信内外网隔离的现状和探测设备保障需求,提出基于远程帧缓冲协议(RFB)的多路并发远程技术支持系统设计。该系统基于TCP/IP可靠数据传输协议,利用远程帧缓冲协议RFB的图像压缩能力和图像重现功能,以及真正的瘦客户技术和平台无关性,克服了内网和外网防火墙对于远程技术支持的壁垒,使远程技术指导、远程技术培训以及无人值守站点的远程监控都能够方便实现。实践证明该系统有效提高了广东省气象探测设备远程保障效率,大大降低了设备维护成本。     

基于复制结构的协同绘图并发控制算法

协同绘图是计算机支持的协同工作(CSCW)的重要研究方向,复制模式下的实时协同图形编辑系统支持不同地域的设计人员通过网络同步高效地浏览、操作和修改各种图形,其中操作意愿保证及其并发控制成为复杂而又关键的问题之一.讨论了基于复制结构的并发控制策略,给出了一个有效的适合图形对象并发控制算法.     

基于人工神经元网络的控制系统模型简化的专家系统

本文研究并实现了一个基于人工神经元网络的控制系统模型简化的专家系统(简称为ESOMRT)。该系统适用于专家和非专家用户,能够针对更体的连续和离散时间的高阶控制系统模型和简化要求选择合适的简化方法,并可对简化质量从时域和频域方面进行评估。在构造这个系统的过程中,作者提出了智能数据库的概念,使用了过程型和人工神经元网络方法相结合的知识表达方式,并利用神经元网络的再学习机制实现了斗自动知识获取,该系统具有三种工作模式和友好的人机界面,使系统的智能水平比较高并有实用价值,现已在IBM-PC/XT和386机上运行。     

基于图文法的并发系统状态测试方法及其实现

在并发系统的研究和开发中，迫切需要一种能正确有效地描述并发系统的动态进程互联结构、动态进程通信和进程演化行为的形式化方法以及基于这种形式化方法的并发系统动态状态的测试手段．本文介绍一种基于图文法模型的并发系统状态测试方法，该方法与描述并发系统结构和行为的图文法模型相结合，构成了一个并发系统开发支持环境．这一方法可根据对并发系统的状态测试要求，在并发系统的运行期自动跟踪和记录并发系统的运行状态和通信情况，使并发系统的开发者可以实时地得到并发系统的运行状态，或者在并发系统运行结束后重演并发系统的状态变化过程.     

Concurrent C及其运行时支撑系统在分布式环境中的实现

本文介绍我们在Ｓｕｎ工作站网络中实现的一种Ｃｏｎｃｕｒｒｅｎｔ Ｃ分布式版本。文章最后给出初步测试结果。     

基于事中反馈的信用卡欺诈检测与防控

信用卡欺诈活动日益猖獗,如何增强欺诈检测能力来规避持卡客户、商家等的经济损失是电子商务发展中至关重要的问题.给出了一个基于事中反馈的信用卡欺诈检测解决方案,其将数据挖掘技术和反馈控制技术联合运用实现实时欺诈检测及防控,以增强欺诈检测能力来减少经济损失.     

ConcurrentC语言在分布式系统上的一种高效实现

本文介绍了ＣｏｎｃｕｒｒｅｎｔＣ语言在一分布式系统上的实现。该实现使用了不同于预编译法的编译器的构造方法，同时将Ｃｏｎｃｕｒｒｅｎｔ Ｃ语言中的进程实现为ＵＮＩＸ进程中的用户级线索，是ＣｏｎｃｕｒｒｅｎｔＣ语言在分布式系统上的一种高效实现。     

基于ACTOR模型的并发面向对象语言AC++

ＡＣ＋＋是用ＡＣＴＯＲ模型建造的并发Ｃ＋＋语言．本文介绍ＡＣ＋＋的设计与实现，着重探讨如何在语义级上平滑地结合ＡＣＴＯＲ模型和普通面向对象语言，提出了“扩充的行为抽象”和“异步创建”等新方法，使新语言既能保持面向对象语言的特性，又能支持ＡＣＴＯＲ模型提供的描述并发计算的能力.