摘要：正确性是并行程序的基础,但是由于它的复杂性,其验证要比串行程序困难得多,因此有必要进行建模并研究其性质.从程序的角度出发,在将基于消息传递的并行程序转换为Petri网模型之后,证明了与并行正确的并行程序对应的Petri网模型应当满足的结构性质,包括强连通性、S-不变量、T-不变量、受控死锁性质以及守恒性,并举例说明了这些性质在并行程序验证中的应用.这些性质可用于并行程序的事前验证,而且避免了使用动态性质进行验证时的状态爆炸问题,从而提高并行程序设计和验证效率.同时这些方法具有良好的可推广性.

摘要：认证协议的成功设计是网络安全领域的关键问题之一,对其进行形式化分析是当前研究的热点.在已知协议的运行模式的基础上,给出了基于Petri网的认证协议分析的具体方法,并通过一个实例说明了该方法的有效性.

摘要：公平性是并行程序正确的主要标准之一,但是并行程序执行的不确定性导致公平性验证较为困难。针对消息传递模式的并行程序,在建立相应Petri网模型的基础上,首先证明了并行程序的公平性与其Petri网模型的公平性之间的关系,然后提出了利用T-不变量判断并行程序公平性,以及通过添加控制库所实现并行程序公平的算法,最后指出了将改造后的模型转换为公平并行程序的方法,并用一个实例进行了验证。

摘要：A new method for designing sequential logic circuits is put forward in this paper. The method is that driv-ing condition for flip-flops is obtained by means of the transition firing condition of petri net and that designing asyn-chronous sequential circuits and synchronous sequential circuits can be unified.

摘要：用Petri网对系统进行建模分析可以揭示被模拟系统在结构和动态行为方面的许多重要信息。首先定义了工作流到Petri网的映射方法;然后结合实际应用设计了一个基于Petri网的天气预报用户管理系统模型,分析验证了该模型的可行性和合理性;最后在此模型的基础上,考虑时间因素给出了一种改进的时间Petri网模型,并定量分析了天气预报用户管理系统中每个可能流程的时间性能。

摘要：若对于一个Petri网的任意两个可达标识,都存在一个标识是从这两个标识可达的,则称该Petri网具有汇合性质。汇合性质在研究Petri网的可达标识集及家态时具有重要的意义,并且重写系统的汇合性与Petri网的汇合性质具有紧密的联系,因此对Petri网汇合性质的研究就显得更加重要了。组合化设计思想是复杂系统建模的一种有效途径,Petri网的组合化研究也甚为人们重视,其中同步与共享合成操作是结构复杂Petri网系统分析的两种有效手段。我们首先分析了Petri网的汇合性质,然后分别讨论了同步合成与共享合成操作对汇合性质的保持问题,并得出了若干结论。

摘要：同步距离是描述2个事件间同步的一个重要的恒定性质,反映了2个变迁之间的独立程度。它对系统的设计、分析和优化提供了很大的帮助。文章研究了Petri网中的同步距离的定义,通过实例分析指出原有定义适用于含有有向回路的网系统。随后将原有定义细化,引入公平性、亚公平性、T-跨来定义新的同步距离。新定义将处于非公平关系的变迁根据亚公平关系分2类情况考虑;对于处于公平关系的变迁根据T-跨分3种情况,讨论了同步距离的求解,并通过实例解决了原有定义存在的问题。

摘要：现有桩承式加筋路堤离心模拟技术存在诸多简化,忽略了模型应力历史的相似性。充分考虑几何布桩、材料特性、荷载及应力历史的相似性,优化设计了高重力场在机固结、插桩与路堤堆载的桩承式路堤离心模型试验方案。提出了对应在机加载过程的数值模拟方法,并分别建立了对应模型尺度和原型尺度的桩承式路堤单桩有限元模型。对比分析表明,模型尺度与原型尺度数值模型的桩土沉降曲线、荷载分担规律、路堤与桩身荷载传递、超静孔压分布均吻合,验证了桩承式路堤离心模型相似设计的正确性与合理性。离心模型试验方案能够反映桩承式路堤的变形发展、土拱效应与荷载传递特性,为在机加载条件下桩承式路堤离心模型试验奠定了重要的先期研究基础。

摘要：基于计算资源共享模型的研究,提出了混合云计算资源市场HCRM(Hybrid Cloud Resource Market)的功能架构,研究了市场管理层的交易管理机制,给出了计算资源的供需质量模型,设计了一种质量感知的双向拍卖算法QaDA(Quality-aware Double Auction)。仿真运行结果表明,与普通的连续双向拍卖算法CDA(Continuous Double Auction)相比,QaDA不仅可以引导用户合理定价,也能获得较高的匹配成功率和较高的交易总额。

摘要：为设计出能够验证并行排序网络正确性的有效工具,根据[0,1]原理和布尔函数的特点和性质,提出一种布尔表达式的化简算法,并根据此算法设计出验证工具。对[0,1]原理和布尔函数的特点和性质进行了讨论,指出有利于化简操作的性质。设计出的工具能够根据并行排序网络的参数显示网络图形、自动生成布尔表达式并实现化简验证,工具的输出有利于对排序网络的分析,也可以用于辅助排序网络的设计和优化。实验结果表明了该工具的有效性。