基于时间约束Petri网的一致性验证算法

时间约束的一致性验证是保证工作流时间模型正确工作的前提,因而一致性验证的算法的精确度和复杂度关乎整个工作流时间模型的运行效率。文中简要介绍了时间约束一致性定义及约束关系的推理规则,提出了一种简洁有效的时间约束一致性验证算法并分析了算法的时间复杂度。该算法借助于T-组件网和时间约束流图,能有效验证时间约束Petri网中存在的各种时间冲突,以保证工作流时间约束模型的建立及运行等各个阶段的正确性,对业务流程的建立、维护和优化都具有重要的参考意义。     

基于时间约束Petri网的一致性验证算法

时间约束的一致性验证是保证工作流时间模型正确工作的前提,因而一致性验证的算法的精确度和复杂度关乎整个工作流时间模型的运行效率。文中简要介绍了时间约束一致性定义及约束关系的推理规则,提出了一种简洁有效的时间约束一致性验证算法并分析了算法的时间复杂度。该算法借助于T-组件网和时间约束流图,能有效验证时间约束Petri网中存在的各种时间冲突,以保证工作流时间约束模型的建立及运行等各个阶段的正确性,对业务流程的建立、维护和优化都具有重要的参考意义。     

考虑任务可达约束的突击作战任务分配方法

在实际突击作战中,航空作战平台进行任务分配时存在任务可达约束的特点。为此,建立任务可达约束条件下突击作战任务分配问题的数学模型。采用遗传算法对该问题模型进行求解,并设计与之相适应的染色体编码方法、随机双点定位的交叉算子和一致性单点调整的变异算子。案例仿真结果表明,该方法能够有效解决任务可达约束条件下的任务分配问题,具有较好的稳定性和时效性。     

一种基于Prolog的时间约束业务流程验证方法

随着互联网技术的快速发展,对复杂系统业务流程建模的需求越来越大。针对带有时间约束的业务流程模型的正确性验证问题,提出了一种基于节点转换规则的图分解算法,将业务流程模型转换为运行时流程轨迹集合;设计了流程轨迹集合到Prolog的转换,将轨迹中的节点与时间约束转化为Prolog事实,提出了一种业务流程模型到Prolog语言的转换算法;将持续时间、周期循环与固定时刻3种时间模式转换为Prolog规则,以其支持业务流程模型3种时间模式的验证。最后对一个带有时间约束的医疗流程实例进行了验证。     

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

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

基于使用场景的时间扩展EFSM建模与完整性验证

为了提高嵌入式实时系统软件的质量和可靠性,采用基于模型的软件测试方法是最有效的途径之一.但是,由于该类软件具有实时特性且十分复杂,一般的模型通常缺乏对其实时特性以及软件行为的描述,且需要丰富的专业领域知识才能将其建立的较为精确完整,导致建模的难度和成本增加,难以保证测试的充分性和有效性.使用场景是用户与软件之间的交互实例,详细描述了软件的系统行为而不关注其内部的复杂结构.因此,为了降低建模的难度,本文基于使用场景的规范化表示Scene来构建模型,并使用时间扩展EFSM模型来描述该类软件的实时特性;为了保证所建模型的完整性,本文设计了模型完整性评估准则,通过验证模型迁移中约束条件的完整性来确定模型是否完整的表征了系统的行为;针对不完整的模型,根据约束条件设计了待补全迁移生成策略生成待补全迁移,并通过动态模拟模型的可行迁移序列执行过程将其补全到模型中,以提高模型的完整性.最后,本文针对4个嵌入式实时系统软件构建时间扩展EFSM模型并进行了一系列的实验.实验表明,本文提出的方法不仅有效的构建了模型,而且能够将生成的待补全迁移有效补全到模型中,进一步提高了模型的完整性.     

作战事件跟踪描述建模及验证方法研究

为了对体系结构设计中的作战事件跟踪描述进行建模分析,提出了用扩展时序图模型对作战事件跟踪描述进行建模的方法。定义时序图的生命线为时间消息,研究了时序图模型与Petri模型之间的同构关系,以此为依据给出了时序图转换为Petri网的算法。在此基础上,研究了扩展时序图和对象Petri网之间的转换算法,并处理了扩展时序图中的自环消息特例。最后,结合防空作战过程给出该方法的一个应用案例。     

OCL约束验证与实现的方法

为了能在运行时验证OCL约束,提出了约束验证框架.针对OCL-Java代码(即OCL约束对应的可执行Java代码)插入的简单方案和封装方法存在的不足,给出了改进的代码插入方案,其中应用异常处理技术从而能够捕获冲突的约束.为了使OCL-Java代码根据设计的代码模式插入到Java程序中,对Java解析器作了修改.最后,实验结果表明了该方法的可行性.     

一种实时系统时间约束验证方法研究

目前,能够对汽车电子领域中复杂嵌入式系统安全关键软件功能模和时间约束分析的方法尚在研究中,而这些系统作为实时控制系统,应该确保其具有准确的、可分析的时间行为。时钟约束规范语言CCSL是实时系统的标准描述语言中描述时钟约束的规范语言。采用CCSL规范表达式描述实时系统时间约束;设计了CCSL基本元素到时间自动机基本元素的转换规则;使用时间自用机验证工具UPPAAL对转换得到的自动机模型进行验证分析,验证实时系统是否满足相应的时间约束。     

基于时间约束网络的智能活动规划

老年人认知能力的下降导致其无法正常规划日常生活的问题已经越来越受到社会的关注。利用信息技术辅助老年人独立完成日常活动,已成为目前一个新的研究领域,其中对其活动的规划和提醒是该领域的一个研究热点。在传统基于时间的活动约束表示和冲突检测的基础上,提出一种更为宽松合理的时间约束,其使活动时间更为灵活,同时引入活动规划中新的活动时间冲突问题。通过时间约束网络的相关概念和理论,将活动规划中冲突检测问题转化为简单时间约束网络是否满足一致性的问题。给出时间约束一致性的一般性检测算法,分析得出活动数较大时其算法复杂度呈指数增长。针对一般性检测算法,提出新的检测时间约束一致性的算法,以降低算法复杂度,解决活动规划中的时间冲突问题。最后通过实验对两种算法的时间复杂度进行了比较。     

Decentralized multi-robot allocation of tasks with temporal and precedence constraints

Abstract

We present an auction-based method for a team of robots to allocate and execute tasks that have temporal and precedence constraints. Temporal constraints are expressed as time windows, within which a task must be executed. The robots use our priority-based iterated sequential single-item auction algorithm to allocate tasks among themselves and keep track of their individual schedules. A key innovation is in decoupling precedence constraints from temporal constraints and dealing with them separately. We demonstrate the performance of the allocation method and show how it can be extended to handle failures and delays during task execution. We leverage the power of simulation as a tool to analyze the robustness of schedules. Data collected during simulations are used to compute well-known indexes that measure the risk of delay and failure in the robots’ schedules. We demonstrate the effectiveness of our method in simulation and with real robot experiments.     

一种基于广播的cache一致性协议的设计和验证

在全互联的网络结构下,提出了一种基于广播的cache一致性协议的详细设计,使请求传输不再像目录协议中的那样,经过第三方中转,而是直接发给所有节点,由最新拥有副本者给出响应。对协议进行了分析证明,并建立了模型,通过模型检测工具NuSMV验证了协议的正确性。     

时空特性约束下的数据挖掘隐私保护方法

在隐私保护数据挖掘的研究中,隐私数据的时间特性以及空间特性是历来研究中常常被忽视的。将数据的安全级与时间性、空间性相结合,引入了数据安全级的时效性及空效性,然后采用层次概化方法进行数据隐私保护处理,并提出了基于时空特性的隐私保护关联规则挖掘算法。最后通过实验对算法的信息损失度、执行时间、算法效能等性能进行了分析和验证。     

时态多维模型设计

传统的数据仓库基于维度时不变的观点,只考虑事实随时间的变化.实际上,数据仓库的多维模式是随时间缓慢变化的.数据仓库多维模式的变化会影响OLAP查询结果的正确性,有必要对多维模式的历史变化进行维护.在分析多维模型结构的基础上,对多维模式的元素进行时态扩展,给出了一种能解决复杂多维结构的时态多维模型的形式定义,并对时态模型更新操作的实现进行了分析,最后对时态模型各元素应满足的时间一致性约束进行了分析.     

Memory-efficient algorithms for the verification of temporal properties

This article addresses the problem of designing memory-efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are modeled as automata on infinite words (Büchi automata). Verification is then reduced to checking the emptiness of the automaton resulting from the product of the program and the property. This problem is usually solved by computing the strongly connected components of the graph representing the product automaton. Here, we present algorithms that solve the emptiness problem without explicitly constructing the strongly connected components of the product graph. By allowing the algorithms to err with some probability, we can implement them with a randomly accessed memory of size O(n) bits, where n is the number of states of the graph, instead of O(n log n) bits that the presently known algorithms require.     

信息系统中业务规则与约束的时态化研究

在OCL和ECA规则的基础上,通过对业务对象与ECA规则的时态化关系的分析,提出了业务规则与约束的一种时态化扩展建模方法,该方法引入了时态化算子和时间区间等概念来实现对时态化对象和属性的历史信息的引用和时态化建模。     

基于集中式存储的全局约束并行相容模型

为了利用多处理平台的并行处理能力, 提高约束求解中相容检查的效率, 提出了一种新的基于集中式存储的全局约束并行相容模型。利用动态分配约束条件的方法解决负载均衡问题; 通过对变量域的集中式管理, 保证了冲突检测的及时性; 利用变量域剪枝单调性的特点, 实现了异步相容检查, 提高了多节点间相容检查的并行程度。最后, 通过实验验证并讨论了模型的优势和适用范围。     

一个支持软件需求验证的过程模型研究

需求验证是软件需求阶段的一个重要环节,未经验证的需求给项目成功带来较大的需求风险。在前期研究的基础上,从需求验证的基本原理和可操作性出发,提出一个支持需求验证的过程模型(RVPM),进行形式化描述,并论述了需求验证过程的几个关键过程和策略。结合实例,分析了如何应用该模型来指导需求验证过程。理论和实例分析表明：该模型有效地克服了需求验证过程的复杂性和经验操作,有效降低项目需求风险。     

自适应软件动态过程时间特性建模与验证方法

现有自适应软件建模与验证方法较少考虑时间约束,然而,在时间攸关应用领域,自适应软件能否正确运行,不仅要考虑自适应逻辑的正确性,还要考虑自适应软件动态过程的时间特性。为此,首先显式定义了自适应软件的时间特性（监控周期、延迟触发时间、自适应过程截止时间、自适应调节时间和稳定时间等）;然后,构造了一种基于时间自动机网络（TAN）的自适应软件动态过程时间特性建模模板;最后,将自适应软件时间特性描述为定时计算树逻辑（TCTL）的形式,并对时间特性进行了形式化分析和验证。结合具体案例验证了该自适应软件时间特性建模和验证方法,结果表明该方法能够显式刻画自适应软件时间特性,降低其形式化建模的难度。     

A temporal programming model with atomic blocks based on projection temporal logic

Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model （αPTL） which extends the projection temporal logic （PTL） to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.