时间约束层次细化工作流建模及验证研究

为降低工作流建模和验证的复杂度，提出了一种自顶向下逐步细化的建模与验证方法。首先，引入了层次细化工作流网，实现复杂工作流建模，将满足可靠性的子网，替换顶层结构中输入库所安全的子网变迁，使细化后的工作流模型自动地满足可靠性要求。为验证可调度性，提出了时间约束层次细化工作流网，给出子网与子网变迁之间的时间约束等价变换原则，可保持细化前后工作流网可调度性不变的充分条件。依此条件，分别给出了串行、并行、选择、循环4种基本组件的压缩推理规则，并在线性复杂度内解决了层次细化工作流网时间验证问题。

Modeling and verification of timing constraint hierarchical refinement workflow

To reduce the modeling and verification complexity in complicated workflow,a top-down refinement method for modeling and verification was proposed.Firstly,the Hierarchical Refinement Workflow net(HRWF-net) was introduced to design complicated workflow in the framework of Petri nets.Those transitions whose input places were safe should be refined by sub nets satisfying reliability to guarantee soundness of resulting workflow net.Furthermore,to verify schedulability in the hierarchical refinement workflow,Time Constraint Hierarchical Refinement Workflow net(TCHRWF-net) was presented,and the range of token's arrival time of the sink place in the sub net was calculated.If the range of token's arrival time equals to that of output place of the transition in the top workflow net refined by the sub net,schedulability of resulting workflow remained unchanged.According to the conclusion,a set of transform rules for four elementary workflow components were proposed,which could realize the time constraint verification of TCHRWF-net within linear time complexity.