并发程序验证的时序Petri网方法

并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一 .Petri网和时序逻辑被认为是探讨该问题较为有效的两个理论工具 ,但二者都有局限性 .该文引用一种新网子类 :时序 Petri网 ,描述了并发程序的时序 Petri网建模方法 :利用网结构描述程序基本框架及保证语句的原子性 ,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系 ,从而有效地对基本网无法描述的并发程序进行了建模 ;在此基础上 ,结合Petri网的可达图分析技术和时序逻辑的演绎公式 。

网上证券交易系统的时序Petri网描述及验证

基于时序Petri网对我国现行网上静态和动态证券交易系统进行了模拟、形式描述及功能正确性验证.应用时序逻辑推理规则,从形式上严格证明了证券交易系统需求规范及其时序Petri网模型动态行为的一致性.结果表明,时序Petri网能够清楚而简单地描述事件间的因果关系和时序关系以及并发系统中某些与时间有关的重要性质,如最终性和公平性.因此,时序Petri网可作为并发系统形式化描述和分析的有力工具.

行车安全综合监控系统的时序Petri网描述及验证

行车安全综合监控系统规模大,复杂程度高,且具有不确定性。研究有效的形式化分析和验证方法对系统测试和可行性分析等方面具有重要意义。本文基于时序Petri网,提出了相应的分析和验证方法。然后,以系统中数据处理和传输过程的公平性、及时性和可靠性等问题为例,进行建模、分析和验证,从而说明本方法的有效性。

基于时序Petri网的联锁逻辑形式建模与验证

时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。

时序Petri网在智能控制中的应用

利用时序 Petri网对实际问题进行建模 ,通过 Petri网反映系统的物理结构 ,并利用时序逻辑公式描述系统需求及其相关约束条件 ,从而通过时序 Petri网的运行 ,得到施加控制后的变迁发生序列 ,即对应问题的实现方案 ,达到智能控制的目的。

基于时序Petri网的火电厂管控信息系统模型研究

为了优化火电厂管控信息系统,提出了基于时序Petri网的火电厂管控信息系统模型研究。首先提出了时序Petri网的分层建模方法,并给出了时序Petri网对复杂系统的建模步骤;其次,建立了整个火电厂管控信息系统的时序Petri网模型;再次,为了更好地分析和优化Petri网模型,对其进行了简化;最后,证明了简化后的时序Petri网大大减少了库所和变迁的数量并保持了原网的功能性。

基于事件起点的层次化时序Petri网及其电网故障诊断方法

电网发生故障后利用大量告警信息快速准确地识别故障元件是保障可靠供电和电网安全稳定运行的首要任务。为适应电网运行调控需求,提出一种基于事件起点的层次化加权模糊时序Petri网故障诊断方法。在完善母线和线路的层次化加权模糊时序Petri网模型的基础上,以故障发生时刻为事件起点,确立各初始库所的时序属性,并通过逆向和正向时序推理对保护和断路器动作信息进行时序约束检查和置信度修正。IEEE 39节点系统仿真算例和电网实际故障算例表明所提方法能够在保护和断路器误动/拒动、告警信息缺失/错误等复杂状态下识别真实故障元件,提高了故障诊断的准确度和容错性。此外所提方法还可以得到设备故障的时间点约束,有利于进一步分析故障原因和故障事态发展。通过与现有应用时序信息的故障诊断方法相比,所提方法时序推理过程简明清晰,对网络拓扑的变化适应性强,运算速度快,满足在线诊断需求。

温控系统的时序Petri网建模与验证

基于时序Petri网对温控系统进行建模和性质描述.利用可达图、Büchi自动机和ω-正则表达式理论三者相结合的方法分析得到温控系统时序Petri网模型变迁引发序列集合的ω-正则表达式,进一步分析证明该ω-正则表达式满足温控系统的功能性需求说明,从形式上验证了温控系统时序Petri网模型与需求说明一致.结果表明,时序Petri网可用来描述和验证具有时序关系和因果关系的并发系统模型,是一种并发系统形式化描述和分析的有效工具.

基于加权模糊的时序约束Petri网电网故障诊断方法

电网发生故障后充分利用报警信息对故障元件进行判别,是保障电力系统安全运行的重要环节。针对现有Petri网时序推理与置信度推理相分开、计算过程复杂且未充分利用时间信息等问题,提出了一种基于加权模糊的时序约束Petri网电网故障诊断方法。将时序约束引入到Petri网的库所与变迁中,根据保护与断路器之间的动作顺序关系建立加权模糊的时序约束Petri网模型。定义置信度与时间区间分层推理运算,实现置信度推理与时序推理同步进行,在置信度推理过程中充分考虑到时间信息的影响。通过对多组算例仿真比较得出,所提方法能够有效判别出故障元件,具有较高的准确性和容错性。

基于时序模糊Petri网的电力系统故障诊断

提出了基于时序模糊Petri网的电力系统故障诊断方法,重点分析了故障诊断模型的特点,给出了电网拓扑结构发生变化时模型的快速修正方法,充分合理地利用了保护和断路器动作信息的时序属性,提出了动作信息不完备情况下的纠错算法,可较好地完成继电保护的动作评价。以14节点系统为例验证该诊断方法的准确性和模型修正方法的快速性。与已有方法的比较表明,该方法诊断速度快、精度高,具有适应电网拓扑结构变化的能力,适用于大型电力系统故障诊断。

利用电气量和时序信息的改进Petri网故障诊断模型

现有的电力系统故障诊断模型在利用多渠道、多方位的测控信息方面,大多采用决策级别的信息融合,在信息冲突或不完整时有可能导致误判;对时序信息的利用一般局限于对信息的初步筛选,未能充分利用时标偏差与信息准确程度之间的关联性。在此背景下,以现有模糊Petri网故障诊断模型为基础,对多源信息进行融合分析,充分利用设备遥信动作事件的顺序记录(SOE)、由广域测量系统得到的电气量信息以及这些信息所包含的时序特性,建立了一种考虑时序信息的多源Petri网故障诊断模型。所发展的故障诊断模型通过利用时序信息对保护设备动作事件进行置信度评价,利用多源信息的冗余度对所缺警报信息进行补充并校验所收到的警报信息的正确性,可以有效提高故障诊断的准确度和可靠性。最后,采用南方电网和江苏电力系统发生过的实际故障案例对所建立的故障诊断模型进行了验证。

计及死区故障的3/2接线变电站的Petri网故障诊断方法

现有针对3/2接线系统的故障诊断方法较少考虑死区故障,在基于保护和断路器动作信息进行故障诊断时易造成误判。提出一种计及死区故障的3/2接线变电站的Petri网故障诊断方法,除了系统中母线、线路和变压器等元件,对死区位置也建立其加权模糊时序Petri网模型。针对3/2接线系统不同死区位置、不同类型故障的跳闸策略,利用保护动作信息和断路器辅助节点开合状态信息构造死区故障辨识逻辑。通过死区故障的逻辑辨识和保护及断路器的时序约束检查,对诊断模型的结构和参数进行修正。测试系统仿真算例和电网实际故障案例表明,该方法能够在保护和断路器不正确动作和警报信息不完整等复杂状态下识别真实故障元件,提高了诊断的准确度和容错性。

时序Ada网的语言性质

在 Ada网的基础上 ,利用时序 Petri网为 Ada任务程序建模 ,提出了时序 Ada网的概念。利用时序 Ada网 ,可以很好地反映 Ada程序的公平性和原子性要求及描述程序的需求规范。对时序 Ada网的语言性质进行分析 ,结论表明时序 Ada网所能接受的网语言能完整地刻画程序的动态行为和时序关系 ,有助于对程序性质的分析和验证。

基于知识流的设计更改执行阶段过程改进

针对设计更改执行阶段效率的问题,从知识传递角度分析了设计更改执行过程中的知识流动机制,结合设计更改执行过程活动的离散并行性、逻辑时序性以及知识显/隐性转化特点,提出了基于改进时序Petri网的设计更改执行过程知识流建模方法和面向知识流分析的知识活动解构方法,建立了设计更改执行过程改进模型。提出了基于KFO-TPN模型的设计更改执行过程关键路径识别算法,以及基于语义信息增益和结构信息增益的设计更改过程知识流动合理性分析方法。以某研制型企业中设计更改单在车间内执行阶段的过程改进为例验证了所提方法的有效性。

审计缓冲区的形式化模型及其验证

审计系统作为安全信息系统的一个重要组成部分,对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分,本文利用时序 Petri 网对审计缓冲区管理的实现方案进行建模,进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了 Petri 网缺乏描述系统事件之间时序关系的局限性,同时发挥了 Petri 网对系统并发和物理结构的有效描述及分析的优势,达到了系统验证的目的。

集成TPN-BG的铝挤压机建模方法研究

铝挤压机系统是一个多液压源、多液压缸的系统,难以使用传统的方法进行数字化建模。为了有效地开展AEM的液压系统设计与性能分析,本文提出一种集成时序Petri网和键合图的铝挤压机建模方法。其中,TPN用于AEM的工序建模,BG图用于液压系统的辅助设计,两者通过有限自动机耦合,可以用于系统全面性能分析。实验结果表明,数字化模型与实际系统具有明确的物理相似性。

CORBA系统事务处理的模拟和分析

事务处理对于建立可靠的CORBA应用系统是很关键的,事务处理已经成为分布式应用系统设计的原则。CORBA的一个重要的服务是OMG的提出了对象事务处理服务OTS(Object Transaction Service),负责将事务处理与对象在ORB层上结合。事务成为分布式对象系统中恢复、一致性、并发的基本单位。用着色时序Petri网模拟和分析CORBA环境下的事务处理。

C^4ISR系统任务实时性的评价方法

提出一种定量评价C4ISR(Command Control Communication Computer Intelligence Surveillance and Reconnaissance)系统任务实时性方法——时序着色模糊时间Petri网(TCFTPN)方法。用时序逻辑公式来限制着色Petri网的变迁引发行为,用模糊时间来表示各工作过程的时延特性和降级工作问题。通过估计在规定的时间内标识从任务开始状态到达任务完成状态的概率来确定C4ISR系统的任务实时性。

Optimization of fault management system in power plants based on DD-RCM and TPN

A method of optimizing the fault management system in power plants based on DD-RCM （resultchain based modeling for digital developing） and TPN （temporal Petri net） is proposed. First, the model of the fault management system was set using DD-RCM. Then, it was transformed to the temporal Petri net model by corresponding rules. Secondly, relationships among all the activities, such as choice, conflict, synchronization and concurrency, were confirmed according to the Petri net model and described employing the reengineering algorithm of incidence matrix. Thirdly, the Petri net model was reduced by combining reduction rules and conflict, synchronization relationships to optimize the fault management system in power plants. Finally, the functionality of the reduced net was proved by the temporal logic of the temporal Petri net.