基于改进谓词/变迁网的飞行方式指示器模型研究

为实现空客320飞行仿真中的飞行方式指示器(Flight Mode Annunciator,FMA)仿真,面向离散事件系统,提出一种基于二阶谓词/变迁网的建模方法,并对FMA建模及仿真验证。分析FMA系统功能特点,确定其可用谓词/变迁网建模,但FMA每当飞行方式改变时附带的白色方框提示使传统谓词/变迁网模型繁杂而难以实现。为简化系统模型,在谓词/变迁网的基础上提出继发网,以此为基础定义了适用于离散事件系统的通用型二阶谓词/变迁网,以FMA为例进行了建模及仿真验证。实验结果表明,二阶谓词/变迁网解决了离散事件系统建模时“系统中每一次状态更新都会激活同一个新事件”带来的传统谓词/变迁网模型结构复杂问题,实现了空客320飞行仿真中的FMA仿真。

变计时过程/变迁网模型及其应用研究

基于过程运行的离散标识(逻辑变量)和剩余时间连续标识(时间变量),提出一种新的混合标识过程/变迁网——变计时过程/变迁网模型.基于该模型,混杂动力学系统离散事件的实时监控、连续子过程的实时调度等问题可得到有效解决.

利用谓词/变迁网证明的一阶谓词逻辑命题

研究了证明一般的一阶谓词逻辑命题的方法,根据网逻辑的思想,利用谓词/变迁网对一般形式的一阶谓词逻辑命题进行了图形表示,提出了2种一阶谓词逻辑命题的证明方法:图形证明法和矩阵证明法。举出一个实际的例子来说明证明思路。

面向代数规约测试谓词/变迁网

针对谓词/变迁网缺乏有效的形式化验证分析技术,基于代数规约测试谓词/变迁网方法,给出谓词/变迁网转换成代数规约语言CASOCC-WS表示的基调的规则,提出基于测试充分性准则深度优先遍历谓词/变迁网生成变迁触发序列的算法和由变迁触发序列构造公理等式的启发式规则.案例研究表明:该方法可以有效地解决测试Pr/T网时自动生成测试用例和自动判定测试结果和可行路径的问题.

等价标识在谓词/变迁网系统可达树规模缩减中的应用

本文通过对哲学家就餐问题的分析，对谓词／变迁网系统可达树规模的缩减问题进行了讨论，分析系统性质，给出等价标识，利用等价标识直接构成可达树，规模大幅度减小。

变迁耦合网的T-不变量求解算法

首先定义了变迁耦合网及相关概念,其次揭示了变迁耦合网N中各个分支网的T-不变量同N的T-不变量之间的关系,根据是否与耦合变迁有关,将N的极小T-不变量分为两类MTS1和MTS2,然后给出了变迁耦合网所有极小T-不变量的求解算法,并给出了两个简单例子加以说明,最后编程实现所提算法并给出初步实验数据。试验结果说明,本文所提算法比现有算法节省大量计算开支。

弱引发三态加时变迁Petri网动态行为分析

文中提出的弱引发三态加时 Petri网比现有三态加时变迁 Petri网更适于模拟分析一类具确定性时间约束和冲突结构的并发系统 ;给出其动态行为形式化描述与分析框架 ;基于此和受控执行概念 ,并结合实际并发系统的一类调度问题 ,研究其动态行为的一些性质 .

基于Horn子句集的Pr/T网可达树的方案求解

问题求解是当今人工智能领域研究的重点,在文中对于能用Horn子句集表示问题求解情境的一类问题,利用谓词/变迁网对其进行建模,详细分析了网系统模型的有界性,并借助网系统的可达树提出了一个求解问题解决方案的算法.最后给出一个例子对算法思想进行说明.

基于 Petri 网和图像识别方法的故障预防系统研究及实施

以国家ＣＩＭＳ工程技术研究中心制造系统为对象，设计并实施了一个制造系统故障预防系统。文中首先提出了制造系统的谓词／变迁网模型，以此为基础设计了基于Ｐｅｔｒｉ网可达性树分析方法和图像识别方法的制造系统故障预防系统，并给出了系统的总体结构图和相应的模块结构图。该故障预防系统已完成实施，在提高制造系统运行的安全性和可靠性方面，发挥了重要作用。

基于Petri网的数据库概念设计模型

在数据库概念设计阶段,E-R图虽然广泛使用,但反映不出对数据的处理要求和数据库的完整性要求。提出了用Petri网建立数据库概念设计模型,把数据及其相关的处理集成在统一的网模型中,而且用事实(死变迁)规范了该模型的数据库完整性。

基于Petri网的多Agent系统建模的研究

多Agent系统正成为分布式自治系统研究的一个热点,并被大量应用在商业和工业软件系统的开发中.这些系统的复杂性表明急需一种系统建模技术来构造多Agent系统,从而支持可靠的、可维护的和可扩展的系统设计.文中分析了Petri网技术在多Agent系统建模领域的应用背景,对基于Petri网的多Agent系统建模方法进行了分类、分析、比较和评估,指出了目前使用Petri网技术对多Agent系统进行建模存在的问题,并给出了今后的研究方向.

基于Petri网的互斥算法

使用库所 /变迁网来描述进程的互斥算法 ,并针对两个进程交替进入临界段算法的不足 。

用Petri网描述进程的死锁

死锁是操作系统的一个重要概念,本文提出用库所/变迁网直观,动态地描述并发进程的死锁,本人将这一方法用于操作系统有关死锁内容的教学取得了非常好的效果。

基于时延Petri网的并行程序的分析

在分析并行程序时,很多问题需要考虑,如通信、同步、数据划分和分配、负载平衡、容错、异构、死锁及竞争等问题,采用一般方法是很困难的。时延Petri网能够很好地描述这些问题,使并行程序的分析变得简单,且有利于并行程序的分割。给出了并行程序的时延Petri网建模方法,并对一个实例进行了分析,得出了并行程序的Petri网模型,对并行程序的分析及验证打下了基础。

基于时延Petri网数据并行问题的分析

Petri网作为一种直观的图形建模工具和一种具有丰富数学基础的形式模型,非常适合描述具有并发、异步和分布特征的系统。数据并行即将相同的操作同时作用于不同的数据,利用时延变迁Petri网来分析数据并行问题,可以找出具有相同操作的结构,这对于数据并行问题在并行机上进行模拟有很大好处。

一种面向对象Petri网的构造及其CAN总线系统的应用

提出一种面向对象Petri网——变迁型面向对象Petri网,是库所型面向对象Petri网的对偶网,并在子网内部设置特殊的库所——条件判断库所来限制消息输入变迁,适用于CAN总线系统的建模。该网通过定义对象子网之间的消息输入和输出变迁来实现相互通信,并对对象的接口进行扩展,采用消息决策控制。最后对CAN总线系统进行建模、分析和验证,并总结这类网模型自身的优点。

Agent系统软件体系结构形式化建模方法

基于Agent技术为复杂分布式问题提供了求解方法。软件体系结构是控制软件复杂性、提高软件系统质量、支持软件开发和复用的重要手段之一。软件体系结构设计可用于描述Agent与Agent之间的交互和组织结构的规划,因此Agent系统能从良好的体系结构设计中受益。该文整合了图表句法理论和层次谓词变迁网理论,提出一种形式化建模方法,从抽象层(架构)和实现层(动态行为)两方面来构建Agent系统的软件体系结构。模型具有可验证和追踪性,为Agent系统软件体系结构分析与评估提供了良好的基础。

软件体系结构动态特征建模与验证

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.

复杂工业过程集成建模及其实时监控与调度

采用一种新的混合标识过程/变迁网模型-变计时过程/变迁网来描述复杂工业过程。该模型通过引入过程运行标志离散标识(逻辑变量)和过程运行剩余时间连续标识(时间变量),有效解决了多工位多工况复杂工业过程底层子过程的集成建模问题、离散事件与连续状态和过程控制与生产控制之间的耦合衔接问题,以及离散事件实时监控、连续子过程实时调度与控制等问题。给出了其实时监控、实时调度与过程控制的最佳策略求解方法。