时序逻辑在有效性控制中的应用研究

工作流系统中的活动是与时间有着紧密联系的,如何保证恰当的活动在恰当时间被执行是工作流系统中的关键问题。探讨了如何利用时序逻辑来解决上述问题,提出了工作流系统中有效性的概念,给出了基于时序逻辑的有效性约束模型,并利用模型检测技术提供了验证有效性约束的方法,最后给出一个实例说明该方法的正确性。     

时间UML-Statecharts建模的工作流时序约束的一致性验证

工作流模型验证已经成为工作流的重要研究领域之一，工作流模型的时间正确性的验证也越来越受到关注。本文通过对于UML-Statecharts进行时间扩展，建立工作流的时间模型，再把该模型转化为时间自动机，最后分别在建立阶段、实例化阶段和运行阶段使用模型检测技术对时序约束的一致性进行验证，检查是否存在相冲突的时序约束。     

基于时间Petri网的工作流模型分析

工作流管理的最终目的是实现适当的人在适当的时间执行适当的活动.企业要获得竞争力,需要在工作流模型中考虑与业务过程相关的时间约束.一个考虑时间因素的工作流模型,需要在投入运行前进行时间规范与验证,以保证工作流执行的时间协调.通过为工作流网元素扩展时间属性,得到集成业务过程时间约束的工作流模型??时间约束工作流网(TCWF-nets).基于对业务活动的可调度性分析,提出了时序一致性验证方法,确保工作流执行中活动之间时间交互的安全性.在所附加的时间约束下,该可调度分析方法不仅能够检测某一给定工作流调度的时间可行性,还能对特定的实例给出一个最优调度,使工作流执行延迟最小.研究结果表明,该方法支持业务过程的时间建模与分析,对于丰富现有工作流系统的时间管理功能以及增强现存工作流软件对动态业务环境的适应性具有重要意义.     

工作流中时序约束正确性验证

分析了工作流管理系统中主要应该考虑的时间问题，然后建立了一个工作流时序条件有向图模型，在该模型基础上进行了一些关于时序逻辑推理问题的研究，提出了4个推理规则，同时提出了验证工作流活动时间约束正确性的一些必要条件。研究结果表明，所作的工作对于工作流管理系统的时间建模，监控和性能评价有一定的参考价值。     

基于构件软件的可靠性通用模型

工作流管理的最终目的是实现适当的人在适当的时间执行适当的活动.企业要获得竞争力,需要在工作流模型中考虑与业务过程相关的时间约束.一个考虑时间因素的工作流模型,需要在投入运行前进行时间规范与验证,以保证工作流执行的时间协调.通过为工作流网元素扩展时间属性,得到集成业务过程时间约束的工作流模型??时间约束工作流网(TCWF-nets).基于对业务活动的可调度性分析,提出了时序一致性验证方法,确保工作流执行中活动之间时间交互的安全性.在所附加的时间约束下,该可调度分析方法不仅能够检测某一给定工作流调度的时间可行性,还能对特定的实例给出一个最优调度,使工作流执行延迟最小.研究结果表明,该方法支持业务过程的时间建模与分析,对于丰富现有工作流系统的时间管理功能以及增强现存工作流软件对动态业务环境的适应性具有重要意义.     

一种基于知识树和约束的柔性活动动态细化方法

柔性工作流在应对业务建模过程中的动态不确定因素、提高工作流系统的柔性具有巨大的优势,然而,柔性活动的动态细化一直是柔性工作流建模和应用的一个难点。因此,提出一种基于知识树和约束的柔性活动动态细化方法。该方法以知识树的包含和泛化关系作为启发信息,以活动选取约束和时序约束作为指导和校验,实现柔性活动的动态细化。在介绍了知识树及其蕴含关系以及活动选取约束和时序约束规则的基础上,给出了柔性活动的动态细化算法,描述了活动选取校验和时序约束校验算法。最后给出了算法的实现和实例分析,其结果表明了所提方法的有效性,能够很好地解决柔性活动的细化问题。     

一种基于Petri网的时间工作流模型的研究与验证

时间管理是工作流管理软件的重要部分，针对目前工作流系统对时间管理的需求，通过对传统Petri网扩展时间信息来描述时间模型，提出了一种静态验证方法，对模型进行基本验证和任务间的依赖约束验证；实例分析表明，该方法在减少工作量的同时提高了验证的有效性。     

芯片开发功能验证的形式化方法

在芯片设计领域,采用模型驱动的FPGA设计方法是目前较为安全可靠的一种方法.但是,基于模型驱动的FPGA设计需要证明FPGA设计模型和生成Verilog/VHDL代码的一致性.同时,芯片设计的正确性、可靠性和安全性也至关重要.目前,多采用仿真方法对模型和代码的一致性进行验证,很难保证设计的可靠性和安全性,并存在验证效率低、工作量大等问题.本文提出了一种新型验证设计模型和生成代码一致性的方法.该方法利用MSVL语言进行系统建模,并通过模型提取命题投影时序逻辑公式描述的系统的性质,通过统一模型检测的原理,验证模型是否满足性质的有效性.进而,应用信号灯控制电路系统作为验证实例,对验证方法做了检验和说明.     

接口时序一致性连续定量监测技术研究

为了解决电气系统接口时序一致性的长期连续定量监测问题,设计了一种基于对比测试的时序一致性监测系统。该系统通过建立时序参数的描述模型将时序约束统一为约束矢量并通过图形化界面输入,约束矢量包含时序参数的测点及约束条件。将理想时序周期内同一事件下各信号的逻辑值编为事件码并按事件先后顺序排列,以事件码序列为码型触发的模式序列,基于设计的DEW-BM算法捕获与模式序列匹配的目标数据序列并计算其中各时序参数的测量值,通过验证测量值是否满足约束不等式给出接口时序一致性的监测结果(Pass/Fail)。测试结果表明,监测系统能够正确捕获目标信号,时序一致性分析结果与理论期望结果一致,监测系统具有一定的正确性和通用性。     

基于π演算的工作流模型检验

为保证工作流模型语义的正确性,提出一种基于π演算的工作流模型语义性质检验方法。采用π演算的一个子集πN演算描述工作流模型,证明该模型的反应关系能够终止,构造有限反应迁移图算法,利用NuSMV检验工作流模型是否满足线性时序逻辑性质。实验结果证明了该检验方法的有效性。     

应用角色访问控制的工作流动态授权模型

形式化地描述了角色、用户、权限、任务单元、授权策略、授权约束等实体及其相互间的关系，提出将授权约束分为需求角色约束、需求用户约束、拒绝角色约束及拒绝用户约束，并在此基础上建立了授权约束的冲突检测规则．实现了授权流与工作流的同步，并通过授权约束的冲突检测确保了工作流的有效执行．文中模型具有全面性与实用性较强的特点．     

云计算环境下聚合服务的随机模型检测

当前缺乏对聚合云服务正确性、响应时间和费用约束统一进行验证的有效方法。扩展基本工作流模式,增强概率、随机、不确定选择的刻画能力,用于定义聚合云服务的服务流程,将流程定义转换为连续时间Markov回报过程,扩展连续随机回报逻辑CSRL,用以刻画增强行为描述的统一验证属性,给出随机模型检测方法。分析表明,该方法能有效刻画运行时云服务动态行为并对其正确性、可靠性进行验证。     

基于时间约束Petri网的工作流动态一致性检验

工作流系统中的时间管理是工作流建模和分析的重要组成部分。支持动态修改是人们在实际应用中对工作流系统提出的新要求。文中在基于时间约束的Petri网模型基础上,根据时间约束推理规则,提出一种动态修改时间约束时检验工作流一致性的方法,从而丰富了工作流的时间管理功能。     

Dynamic checking of temporal constraints for concurrent workflows

At present, workflow management systems have not sufficiently dealt with the issues of time, involving time modelling at build-time and time management at run-time. They are lack of the ability to support the checking of temporal constraints at run-time. Although some approaches have been devised to tackle this problem, they are limited to a single workflow and use only static techniques to verify temporal constraints. In reality, there are multiple workflows executing concurrently in a workflow management system. There may well exist resource constraints between these concurrent workflows, which affect significantly the verification of temporal constraints at run-time. This paper proposes a novel approach for dynamic verification of temporal constraints for concurrent workflows. We first investigate resource constraints in workflow management systems, and then define concurrent workflow executions. Based on these definitions, we propose a verification method by analysing the temporal relationship and resource constraints between activities among concurrent workflows.     

包含时间约束的作战任务建模与验证方法

制定作战计划时往往需要考虑作战任务的时间约束问题。目前对作战任务的时间约束分析方法都存在约束类型少、验证方法适用范围小等问题。为此提出基于业务流的作战任务时间约束建模方法,构建了作战任务流模型并用以描述作战任务的相对和绝对时间约束。提出了作战任务的时间约束形式化验证方法,设计了作战任务模型到NuSMV语言的转换算法,并基于时序逻辑给出了作战任务的基本时间约束描述方法。最后以登岛作战任务为例,验证了其相对约束和绝对约束的部分性质,并根据反馈结果对模型进行了修正。     

联锁逻辑形式化模型检验的研究

利用自动机理论模型检验算法，检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑，有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力，利用该方法对车站联锁逻辑的实际问题进行了性能验证。     

Hyper temporal networks

Simple Temporal Networks (STNs) provide a powerful and general tool for representing conjunctions of maximum delay constraints over ordered pairs of temporal variables. In this paper we introduce Hyper Temporal Networks (HyTNs), a strict generalization of STNs, to overcome the limitation of considering only conjunctions of constraints but maintaining a practical efficiency in the consistency check of the instances. In a Hyper Temporal Network a single temporal hyperarc constraint may be defined as a set of two or more maximum delay constraints which is satisfied when at least one of these delay constraints is satisfied. HyTNs are meant as a light generalization of STNs offering an interesting compromise. On one side, there exist practical pseudo-polynomial time algorithms for checking consistency and computing feasible schedules for HyTNs. On the other side, HyTNs offer a more powerful model accommodating natural constraints that cannot be expressed by STNs like “Trigger off exactly δ min before (after) the occurrence of the first (last) event in a set.”, which are used to represent synchronization events in some process aware information systems/workflow models proposed in the literature.     

Specifying and Validating Data-Aware Temporal Web Service Properties

Most works that extend workflow validation beyond syntactical checking consider constraints on the sequence of messages exchanged between services. These constraints are expressed only in terms of message names and abstract away their actual data content. We provide examples of real-world "data-aware" Web service constraints where the sequence of messages and their content are interdependent. To this end, we present CTL-FO⁺, an extension over computation tree logic that includes first-order quantification on message content in addition to temporal operators. We show how CTL-FO⁺ is adequate for expressing data-aware constraints, give a sound and complete model checking algorithm for CTL-FO⁺, and establish its complexity to be PSPACE-complete. A "naive" translation of CTL-FO⁺ into CTL leads to a serious exponential blowup of the problem that prevents existing validation tools to be used. We provide an alternate translation of CTL-FO⁺ into CTL, where the construction of the workflow model depends on the property to validate. We show experimentally how this translation is significantly more efficient for complex formulas and makes model checking of data-aware temporal properties on real-world Web service workflows tractable using off-the-shelf tools.