一种并发Java程序控制流模型

研究了并发Java程序控制流模型的建模问题.通过深入分析并发Java程序设计语言的语义以及带抑止弧Petri网的建模能力,提出了一种并发Java程序控制流模型--CJCFM,并给出了从并发Java程序构造该模型的方法.CJCFM以带抑止弧Petri网为基础,简单直观,可模拟程序实际运行过程,对并发程序的理解、分析和测试有很大帮助.通过对现有开源Petri网实验平台PIPE的功能进行扩展,可在该平台中直接构造并执行CJCFM.借助成熟的Petri网理论与算法,可验证CJCFM的各种性质,从而达到对源程序进行分析的目的.实验表明:CJCFM能有效协助理解、分析和测试并发Java程序.     

时态逻辑与并发程序

分别阐述了基于Ｍａｎｎａ－Ｐｎｕｅｌｉ框架的命题线性时态逻辑ＰＬＴＬ和基于共享变量方式的并发程序（转换图）模型,并给出该模型与转换系统之间的对应关系;将时态逻辑与公平转移系统ＦＴＳ相结合来描述并发程序及其性质（公平性、安全性及活性）;指出了时态逻辑具备其它形式化方法（ＦＳＭ、Ｐｅｔｒｉ网）所没有的一些优势。     

A heuristic method for temporal analysis based on petri net

Reachability-based analysis and temporal analysis are used to verify the properties of concurrent systems, and it is important to exploit fast and efficient methods. This paper gives semantics of temporal formulae with edges of the transition system of Petri net, and then presents a fast temporal analyzing method, which takes advantage of both Petri net and temporal logic. The method only expands a path of equivalence trace while the path does not satisfy a property according to trace semantics of Petri net, and can validate directly the property on Petri net. Moreover, we exploit a minimal degree of in-out of a node as heuristics to select a path of an equivalence trace. Finally, we demonstrate the validity of the method that decreases state spaces and improves the verification system with the experimental results. Foundation item: Supported by the National Natural Science, Foundation of China (90104005, 66973034) Biography: Fu Jian-ming (1969-) male, Ph.D, research interest: high-speed information network and system safety.     

真并发等价性下的流程模型转换方法

针对工作流建模过程中流程模型的演化问题,在真并发等价性概念下,提出将图形化控制流模型转换为顺序与并发结构可分隔处理的可分离形式的方法.采用自由选择工作流网建模控制流模型,以完全并发互模拟为真并发等价概念,定义两个安全网间是完全并发互模拟关系的充分条件;基于Petri网的网展开,提出获得工作流网的可分离形式的局部网展开算法;通过证明局部展开网与原工作流网满足完全并发互模拟的充分条件,保证两个网模型的等价性.所提转换方法与已有方法相比,能够保留并发层次,且所需步骤更少,有利于流程模型的演化.     

An Algorithm to Construct Concurrent Reachability Graph of Petri Nets

IntroductionPetrinetisausefultooltomodelaconcurrentsystemandanalyzeitsproperties.[1]ThetheoryofPetrinetshasdevelopedsoundlysinceitwasputforwardin1962andwaswidelyappliedtomanyfieldssuchasflexiblemanufacturingsystem,workflow,webservice,etc.[234]ReachabilitygraphisapowerfultooltoanalyzethedynamicpropertiesofPetrinets,bywhichthefiringofconcurrenttransitionsinPetrinetsisrepresentedinaserialmanner.Thatis,Petrinetitselfisaconcurrentmodel,whileitsreachabilitygraphisserial.Infact,concurrencyrelations…     

Horn子句逻辑程序的Petri网模型

Horn 子句逻辑程序 H 可以逻辑等价地转化为 Petri 网模型 M,在 M 中从初始标识 N_0到目标变迁/g(?)形成的发射序列对应着求解 H 的调用序列,在 M 中存在变迁不变式 X≥(?),并且 X(tg)≠0是 H 有解的充要条件。     

FPGA组合逻辑程序的Petri网建模方法

针对现场可编程门阵列(FPGA)组合逻辑程序,提出其普通Petri网建模方法.首先,将状态变量描述为库所对,程序中的逻辑运算描述为变迁,从而将系统程序转换为一个普通Petri网结构;然后,根据Petri网的动态分析性能,给出系统状态可达图的计算方法,实现了状态可达图等价描述FPGA组合逻辑系统运行过程.研究结果表明:该Petri网能够准确地描述变量间的逻辑关系,提出的方法可以为FPGA组合逻辑程序的形式化设计和验证提供建模依据.     

一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法

形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一,尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作,以自定义泛型抽象顺序设计语言Apla为基础,进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言,使其既支持顺序算法的验证又能有效地验证并发分布式算法.在依赖-卫式推理的基础上,提出一种新颖的2层并发分布式算法形式化验证方法,其中系统层用于处理并发级验证,而组件层用于处理顺序级验证.最后,通过2个实例验证了该方法的有效性和可行性.     

基于PPTL的着色Petri网的模型检测方法

为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法。通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足。利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力。     

基于改进的网重写系统的Petri网逻辑控制器的自重构方法

提出一种基于改进的网重写系统的可重构制造系统的Petri网模型的自重构方法。通过改进,克服了网重写系统的若干固有缺陷,提出了Petri网逻辑控制器的自重构方法,这种方法能保证重构中逻辑控制器的正确性,避免复杂的数学分析验证。通过可重构制造单元的实例演示了该方法,并验证了其有效性。     

并行工程过程研究

过程、计算机支持系统和组织管理是并行工程的三个关键问题,在对设计过程进行详细分析的基础上,利用Petri网作为表达工龄,建立了并行工程的过程模型,形式化地表达出并行工程中设计和制造活动在信息意义上的并行性,为并行工程过程的仿真和评价提供了理论依据。     

无刷直流电机DSP逻辑控制程序的Petri网设计方法

提出一种无刷直流(BLDC)电机数字信号处理(DSP)逻辑控制程序的Petri网设计方法.首先,建立霍尔传感器和电机旋转方向的Petri网模型;其次,利用功率管(MOSFET)二二切换规则,设计功率管通断的变迁,获得电机的逻辑控制Petri网模型,并根据Petri网可达图算法,计算无刷直流电机动态系统的状态集合,并利用换相逻辑逐个验证;最后,借助Petri网变迁的激发规则,设计无刷直流电机DSP逻辑控制程序,并对文中方法进行实验验证.结果表明:文中方法能够保证控制程序的正确性和可靠性,可以有效地简化无刷直流电机DSP逻辑控制程序的调试过程.     

Petri网-VHDL编译程序的构造

Petri网适合于异步并发系统建模,将Petri网转换成硬件描述语言,就可以通过EDA工具来实现Petri网控制器．文中给出了Petri网-VHDL编译程序的构造方法．使用CONPAR语言对Petri网进行描述,获得Petri网的CONPAR格式文本文件;由编译软件FLEX生成的词法分析程序产生相应的单词,并将单词传给BYACC程序;再由BYACC程序识别出这些单词,并以自底向上的方式进行归约,形成一棵抽象语法树;最后,自顶向下遍历这棵抽象语法树,将Petri网的CONPAR格式文本转换为VHDL代码．文中给出了一个实例,将编译获得的VHDL代码,通过EDA软件工具MAX PLUSⅡ编译、仿真、综合并下载到系统可编程器件中,仿真波形和试验结果都证明了这个编译程序的正确性．     

混流制造系统的Petri网建模与仿真研究

以赋时Petri网为分析工具,将混流制造系统工艺流程、产品类型标识、缓冲区和加工时间等用基本Petri网语言表示,建立了基于赋时库所Petri网的混流制造系统模型,从全局观点描述事件之间的顺序、并发和同步等关系,并基于该模型,进一步分析混流制造系统的性能,包括操作间的逻辑约束关系、资源冲突、生产能力和设备利用率等.相关实例的仿真结果证明了该模型的有效性.     

Research on Petri Net System Parallel Subnet Partitioning Completeness Theory and Algorithm

In order to solve the parallel algorithm of Petri net system with concurrent function, so as to achieve the parallel control and simulation operation of this system, this paper proposes the function partition completeness theory and algorithms of Petri net parallelization, thereby providing the theoretical support for the realization of Petri parallel algorithms. Firstly, according to the concurrent characteristics of Petri net model, we analyze the parallelism of Petri net system; then, by giving the solving process of place invariants and the function partitioning of Petri net, we propose the function partitioning conditions and determination theorem of Petri net parallelization, and conduct its theoretical proof and practical verification. On this basis, we conduct the theoretical study and analysis on the situation that Petri net system has several kinds of parallel function partitioning, propose the completeness theorem of parallelism function partitioning in Petri net system, and verify it. Finally, we give the algorithms, application examples and simulation experiment results of parallel function partitioning of Petri net systems based on place invariant. The theoretical proof and experimental results show that the function partitioning conditions and completeness theory of Petri net parallelization based on place invariant are correct, and the parallel algorithms under such theoretical basis are also correct and effective.     

并发CHILL源语言调试器的研究

CHILL 语言的重要功能之一就是支持并发。并发的引入使得 CHILL 语言的调试变得十分困难。本文讨论了并发程序调试的困难与问题,研究了一般并发程序调试器应具有的功能,说明了我们借助实时扩展 UNIX 操作系统(RTU)所设计的并发程序调试器结构,找到了扩充的传统调试法用于并发程序调试时一些重要功能的实现方法。实验性地实现了 CHILL 并发源语言调试器。为消除探测影响,本文提出了硬件辅助软件调试法的设想。     

基于用例的层次Petri网建模

利用用例解决了层次Petri网建模中问题界定和问题细化的两个难点，同时也利用层次Petri网表现了用例中文本形式事件流所无法表现出事件自身的并发关系，由此建立的模型具有粒度可控和模块化良好的优点。     

数据库系统并发控制的扩展有色Petri网方法

加锁与可串行化是并发控制中采取的2个主要措施.两段锁协议(two-phase locking protocol,简称2PL)是解决可串行化调度较好的方法之一,但满足可串行化的调度可能会出现死锁.为此建立了多个事务并发访问数据库的扩展有色Petri网模型,该模型可使并发事务的调度符合两段锁协议.利用该模型的可达标识图,给出了判断满足两段锁协议的调度是否死锁的充分必要条件,并由此构造出并发事务的无死锁的可串行化调度.     

RSMC:A Safety Model Checker for Concurrency and Memory Safety of Rust

Rust is a system-level programming language that provides thread and memory safety guarantee through a suite of static compiler checking rules and prevents segmentation errors. However, since compiler checking is too strict to confine Rust's programmability, the developers prefer to use the keyword "unsafe" to bypass compiler checking, through which the caller could interact with OS directly. Unfortunately, the code block with "unsafe" would easily lead to some serious bugs such as memory safety violation, race condition and so on. In this paper, to verify memory and concurrency safety of Rust programs, we present RSMC(Safety Model Checker for Rust), a tool based on Smack to detect concurrency bugs and memory safety errors in Rust programs, in which we combine concurrency primitives model checking and memory boundary model checking. RSMC, with an assertion generator, can automatically insert assertions and requires no programmer annotations to verify Rust programs. We evaluate RSMC on two categories of Rust programs, and the result shows that RSMC can effectively find concurrency bugs and memory safety errors in vulnerable Rust programs, which include unsafe code.