复杂信息系统流程验证及统一建模平台实现研究

摘要

复杂信息系统的流程复杂，并发性强，分支结点多，系统完成后发现系统存在问题，更改系统代价会很大，所以应对系统进行建模，检查系统流程中存在的死锁和活锁。业务流程管理倡议组织(BPMI，The Business Process Management Initiative)开发了一套标准的业务流程建模符号(BPMN-Business Process Model and Notation)，它是一套图形化和用户友好型业务流程符号。但是，由于BPMN是半形式化型语言，自身无法进行推导演算来查找模型中存在的问题，所以，需要提出方法对BPMN模型进行验证。而模型检测是对状态空间的穷举搜索，对于并发性强的复杂信息系统来说，状态爆炸是不可避免的，所以，应该找出减小状态爆炸几率的方法。
　　为了解决业务流程设计、形式化分析、验证的平台不统一，可移植性差等问题，提出了一种在统一建模平台上处理BPMN模型输出的业务流程形式化验证方案。首先构建基于Java语言的形式化建模平台，将BPMN模型输出作为该平台的输入，随后输出基于BPMN2.0业务流程形式化验证的Java程序代码；该代码可在本文构建的建模平台实现自动检验业务流程模型中可能存在的死锁、活锁，并通过设置“截止点”来解决由活锁引起的状态爆炸问题。文中最后给出了复杂信息系统的相应的实例，验证了方案的有效性。下面是本文主要研究的几个方面，包括：
　　1.分析了Petri网和π-演算的业务流程验证方法，总结出BPMN模型的核心元素到Petri网的映射以及BPMN模型核心元素到π-演算的映射，得出这两种验证方法存在平台不统一问题，并提出在统一Eclipse平台上建模BPMN业务流程并完成验证工作的方法。
　　2.根据各种验证算法的映射思想将BPMN模型的核心元素封装成java类后，建模的BPMN模型可先转换成java代码，然后对**.java文件进行死锁和活锁的验证。
　　3.在展开算法中加入“截止点”的标识，当流程识别到“截止点”时终止对流程中相同路径的遍历，从而减小状态爆炸的几率。
　　通过比较统一建模平台的BPMN业务流程验证、Petri网验证BPMN业务流程与π-演算验证BPMN业务流程，得出前者可以在统一平台中完成整个建模与验证的工作，简化验证步骤；通过比较BPMN业务流程验证和Petri网验证BPMN业务流程的图元个数和路径个数，得出BPMN在描述复杂系统时复杂度相对较低，可通过减少状态空间和搜索路径来减小状态爆炸几率。