并发软件系统的WFD-net模型及偏序展开分析方法研究

伴随着高并发技术的推广以及智能应用需求的增大，传统的并发软件系统分析方法正面临诸多新型挑战。尤其是在数据流程分析方面，它们往往利用交错语义理论来进行相关性质验证与数据错误检测，如状态迁移图、可达标识图与时序逻辑等。由于这些交错语义方法大多需要考虑业务活动的全局顺序并通过遍历系统的全局状态来对系统行为进行分析，因而很容易遭受状态空间爆炸、并发语义缺失以及伪状态等问题。为了解决以上问题，本项目创新性地采用基于并发语义理论的偏序展开方法来对并发软件系统的数据流程进行分析与检测。主要研究内容包括：(1)基于WFD-net的并发软件系统建模方法；(2)并发软件系统模型的偏序展开理论；(3)基于偏序展开的数据流程错误检测方法。此外，设计开发出相应的模型检测器用以验证相关理论方法的正确性与有效性。通过本项目的研究成果可提高并发软件系统的数据流程分析效率，为后期产业系统的实际应用提供科学高效的解决方案。

Driven by high concurrency and intelligent applications, the traditional model-checking methods of concurrent software systems are faced with many new challenges. No matter state transition diagrams or temporal logics, these methods are based on the interleaving semantics. They usually consider the general orders of business activities, and utilize the global states of concurrent software systems to analyze their behaviors. Hence, these methods easily suffer from the problems of state space explosion, lacks of concurrency relations and pseudo states. In order to overcome these problems, this project innovatively uses the partial-order unfolding technique of Petri net to analyze the data-flows of concurrent software systems based on the concurrency semantics. The main studies of this project are as follows: (1) the modeling of concurrent software systems based on WFD-net (Workflow net with Data); (2) the partial-order unfolding theory of concurrent software systems; and (3) the detection method of data-flow errors based on the unfolding techniques. Additionally, a model checker is developed to verify the correctness and effectiveness of our methods. The research achievement of this project can increase the analysis efficiency of data-flows, and guarantee the correctness and reliability of concurrent software systems. Furthermore, some scientific and efficient solutions can be provided to our industry systems.