移动计算系统的变结构Petri网模型及分析方法研究

Mobile computing system has characteristics of concurrency, interaction and mobility. Its advent has changed not only the people’s way of life and work, but also our understanding of computation. It is a great challenge for computer science in recent years to understand the mobile computing system, establish a strict mathematical model for it and thus provide theoretic foundation for the design and analysis of actual system. Therefore, this project will focus on two key science problems: the construction of the formal model for the mobile computing system and the analysis and verification methods for the mobile interactive correctness, start with formal methods, design a variable-structured Petri net, and construct a uniform Petri net model that is suitable for describing the mobile computing system; then develop a set of analysis and verification methods on the basis of the constructed model, propose the state analysis method of the variable-structured Petri net and the property verification and control technology based on net operations, present the behavioral theory of the mobile computing system and the predictability analysis technology of interactive behaviors, realize the analysis and verification of the mobile interactive correctness in systems; and finally develop the study on the application verification of mobile transaction payment systems. The research of this project will provide a theoretic method for the design and implementation of mobile computing systems, enrich and develop the scientific theory of mobile computing, and offer the technical support for the better application of mobile computing.

移动计算系统兼具了并发性、交互性和移动性，它的出现在改变了我们生活和工作方式的同时，也改变了我们对计算现象的认识。如何理解移动计算系统，为其建立严格的数学模型，从而为实际系统的设计和分析提供理论基础，是近年来计算机科学面临的重要挑战。为此，本项目从形式化方法入手，围绕移动计算系统的形式模型构建和移动交互正确性分析验证方法两个关键科学问题，设计变结构Petri网模型，构建基于变结构Petri网的移动计算系统模型；进而发展一套基于模型的分析验证方法，提出变结构Petri网的状态分析方法与基于网运算的性质验证和控制技术，建立移动计算系统的行为理论及交互行为的可预期性分析技术，实现系统移动交互正确性的分析验证；最后开展移动交易支付系统中的应用验证研究，研制相应的建模与分析验证工具。项目的研究，将为移动计算系统的设计和实施提供理论保障，丰富和发展移动计算科学理论，为移动计算的更好应用提供技术支撑。

近年来，移动计算系统已经成为了一些关键系统，例如贸易、航空航天和医疗健康等系统的核心。但由于系统中组件的移动性、组件间的频繁断接性等特征，系统行为变得十分复杂，这对于系统中正确性和可靠性的验证提出了更高的要求。但是目前仍然缺乏能够完整刻画并发、交互和移动性的易扩展的Petri网模型；与此同时，现有的模型分析验证方法存在较大空白，大多局限于状态枚举。因此，本项目从移动计算的本质特性入手，1）定义了一类新的面向移动计算系统的Petri网模型——可变Petri网（VPN），引入虚库所来抽象可能的接口，并增加两个新函数来模拟系统中的链接能力，从而使得模型更加简单的同时擅长描述系统中的动态交互，具有较好可扩展性和可插拔性。2）基于VPN模型，自底向上构建了移动计算系统的两层模型——组件网和交互结构网，并通过网综合构造出完整的系统模型；基于系统模型，提出了系统中的三类必要特性：系统连接性、交互合理性和数据有效性，并给出了其形式化定义。3）提出了系统状态分析方法：研究了VPN的配置树生成算法，给出了可达性、死锁等性质分析定理，并进一步研究系统三类特性的验证算法；研究了系统死锁检测和控制技术；提出了系统移动组件的交互模型与控制方法。4）研究了系统行为分析方法：提出了VPN的系统（交互）行为语言及表达式，提出了行为相关性概念；针对关于系统连接行为/状态的需求，研究了VPN的基于Kripke结构的模型检测方法；研究了Petri网的行为一致性的分析方法；提出了一种将系统行为转换成精确Petri网模型的学习和辨识方法；针对行为的可预期性，提出了一种支持变化影响分析的演化软件建模和模型检测方法。5）基于上述成果，在Web服务、多agent系统和移动交易支付系统中开展应用验证，提出了扩展的VPN模型及相应的分析方法。开发了VPN的图形化辅助软件，实现VPN的绘制、配置树生成、死锁检测以及模型检测功能。项目在国内外学术刊物和会议上共发表论文（含录用）20篇，其中IEEE系列汇刊4篇，ACM CSUR 1篇，SCI检索13篇，EI检索18篇，出版专著1部。申请发明专利3项，获软件著作权1项，培养1名博士、5名硕士。相关成果获2017年中国专利优秀奖和2019年吴文俊人工智能技术发明一等奖，项目负责人丁志军教授入选2020年高校计算机专业优秀教师奖励计划。