业务流程的形式化设计与验证

针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.      

软件体系结构动态特征建模与验证

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.     

命题投影时序逻辑并发建模与自动验证

针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.     

卡银行系统业务模型的分析和建立

笔者针对卡银行系统进行业务建模,得到卡银行系统的概念模型、逻辑模型和物理模型。通过探讨卡银行系统业务系统架构以及业务流程实施方法,阐述了采用标准化流程引擎实现SOA架构的系统整体解决方案。研究还讨论了流程引擎的抽象模型以及三种主流开源工作流引擎,并比较了各自的优劣。以上研究的成果验证了本实验室自创并一直沿用的SOA三层模型建模方法的有效性。     

业务流程建模与测试方法研究

针对复杂业务流程设计测试效率低、自动化程度不高、测试用例正确性难以保证的问题,在研究接口自动机模型的基础上,提出了一种基于模型的业务流程测试方法。该方法首先采用扩展带约束的接口自动机对业务流程设计进行形式化描述,并给出了从业务流程设计模型到带约束的接口自动机模型的转换算法;然后基于模型完成了对业务流程设计与需求的一致性验证,将验证后的接口自动机模型作为业务流程的测试模型,通过其特有的"乐观方法"和博弈思想实现了流程间的嵌套调用组合;最后定义了业务流程的测试覆盖准则,并在满足活动约束条件组合覆盖准则的前提下,设计了相应的测试用例生成算法。实例分析表明:该方法能够简化测试过程,可用于业务流程设计的测试用例自动化生成,有效保证了测试用例的正确性,提高了测试效率。     

PPTL模型检测器实现的一个关键技术

针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.     

UML 顺序图的一种形式化描述方法

统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。     

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

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

基于本体的车间业务流程知识分析及表达

如何有效利用现有业务流程是车间生产管理研究的重点之一.将本体论引入车间的业务流程管理中,探讨了流程知识的构建和表达方法.通过分析车间业务模型,建立了车间本体元模型;再由业务流程的形式化描述,构建了以流程为中心的车间本体模型;利用本体建模语言OWL实现了车间中某具体业务流程的表达,由此来验证所构建的车间本体模型适合于车间知识的表达和共享.结果表明,该方法能便利地实现车间现有业务流程的本体表达.     

一种面向业务过程管理的企业资源模型

目的解决业务过程管理系统中过程建模与过程执行过度耦合的问题。方法通过对组织机构/角色模型的分析,提出了将过程控制逻辑进一步分解为路由逻辑与管理逻辑的思想,提出了描述管理逻辑的企业资源模型并进行了形式化描述。结果通过把企业中的功能作为一种资源由资源管理系统进行管理,实现了路由逻辑与管理逻辑的分离,使过程定义与执行之间的耦合程度大大降低。结论基于企业资源模型的业务过程管理系统,具有模块更清晰、柔性更突出、分解粒度更小等优势。     

医疗业务系统改造中的逆向工程方法

医院信息系统可以使用数据交换或者业务过程管理(BPM)的方式实现。它们的差别在于数据交换方式没有将业务逻辑与控制逻辑分离,而当业务过程改变时,需要更改代码适应。为充分利用这种已有的系统代码资源,将其升级、改造成BPM系统,该文分析了现有系统的实现方式,提出了一种基于过程挖掘的改造方法建立过程模型、提取组织知识以配置BPM系统。最后使用湖南省望城县计划生育服务站的站内系统改造的实例验证了该方法,并说明了具体的升级过程。相对于直接由人工进行升级的方法,该文中的方法更加方便快捷。     

Multi-agent Belief, Goal and Exceptions Reasoning

Temporal logics are often adopted as basic tools to specifying mental states such as belief and goal of agents. Althoush there are works on non-monotonic extension of linear temporal logic (LTL) and branching time temporal logic (CTL), the non-monotonic extension of alternating-time temporal logic (ATL) which is an important kind of multi-agent cooperation logics has not been discussed yet in literature. To solve this problem, this paper proposed non-monotonic alternating-time temporal logic with belief and goal, namely N-ATL-BG, to facilitate the non-monotonic reasoning of mental states of agents. The semantic model, syntax and semantics of this new logic are developed. A model checking algorithm which can be finished in polynomial time is proposed for this new logic. Examples are given to show its usage.     

基于仿真方法验证IDEF3过程模型的有效性

经营过程建模中对模型的有效性验证是过程分析优化的基础。现有的过程模型有效性验证方法单纯追求算法的高效率,只能针对特定模型验证某些过程结构的合理性,不适合经营过程的复杂性需求。该文提出了一种基于仿真方法的有效性验证算法,在确保验证算法效率的基础上,能够验证扩展的IDEF3过程模型的3种逻辑错误:结构死锁、同步丢失和对象不匹配,从而不仅能够验证过程逻辑结构上的不合理,还能够对参与过程的对象所造成的不合理进行验证。     

可重构第三方物流信息系统框架研究

物流信息系统正日益成为物流企业发展的关键．分析了第三方物流业务形态的多样性、业务流程模型多样化及其全球供应链一体化信息集成对系统重构的需求，提出了基于构件的可重构的第三方物流信息系统．采用领域工程思想，探讨了构件化软件方法．在方法的指导下，通过领域分析建立了第三方物流业务构件系统模型，在此基础上实现了一个可重构的层次化第三方物流信息系统框架．该框架可以满足不同物流企业的业务形态，以重构支持业务流程的变化及系统集成．     

一种基于UML的信息系统需求分析方法

针对目前信息系统开发中,需求分析经常遇到的难题,提出了一种基于UML的信息系统需求分析方法,给出了一个需求分析框架,通过活动图技术来对业务流程建模,用对象图模型、状态图模型、交互图模型来构造系统的领域模型.讨论了业务建模、用例的提取、用例的集成等关键技术的实施步骤,使该方法具有更强的可操作性.