基于时序逻辑的业务过程约束建模及验证*

提出一种可视化的约束规则建模语言(visual constraint modeling language, VCML),采用XYZ/E语言作为逻辑框架,统一定义约束规则和业务过程两种模型的形式化语义,为约束规则的自动验证提供形式化基础;然后基于模型检验(model checking)技术,简要讨论模型自动验证的实现方法;最后通过一个应用实例说明业务过程约束的建模。     

Implementing temporal integrity constraints using an active DBMS

The paper proposes a general architecture for implementing temporal integrity constraints by compiling them into a set of active DBMS rules. The modularity of the design allows easy adaptation to different environments. Both differences in the specification languages and in the target rule systems can be easily accommodated. The advantages of this architecture are demonstrated on a particular temporal constraint compiler. This compiler allows automatic translation of integrity constraints formulated in Past Temporal Logic into rules of an active DBMS (in the current version of the compiler two active DBMS are supported: Starburst and INGRES). During the compilation the set of constraints is checked for the safe evaluation property. The result is a set of SQL statements that includes all the necessary rules needed for enforcing the original constraints. The rules are optimized to reduce the space overhead introduced by the integrity checking mechanism. There is no need for an additional runtime constraint monitor. When the rules are activated, all updates to the database that violate any of the constraints are automatically rejected (i.e., the corresponding transaction is aborted). In addition to straightforward implementation, this approach offers a clean separation of application programs and the integrity checking code     

A general treatment of dynamic integrity constraints

This paper introduces a general, set-theoretic model for expressing dynamic integrity constraints, i.e., integrity constraints on the state changes that are allowed in a given state space. In a managerial context, such dynamic integrity constraints can be seen as representations of “real world” constraints and business rules. This topic has important practical applications in many business areas. The notions of (direct) transition, reversible and irreversible transition, transition relation, and consistency of a transition relation will be introduced. The expected link with Kripke models (for modal and temporal logics) is also made explicit. Several practical examples of dynamic integrity constraints will illustrate the applicability of the theory. Some important subclasses of dynamic integrity constraints in a database context will be identified, e.g., various forms of cumulativity (which can be regarded as “transitional” inclusion dependencies concerning two different “points in time”), non-decreasing values, integrity constraints on initial and final values, life cycles, changing life cycles, and transition and constant dependencies. Several formal properties of these dependencies will be derived. For instance, it turns out that functional dependencies can be considered as “degenerated” transition dependencies. Also, the distinction between primary keys and alternate keys is reexamined, from a dynamic point of view.     

Processing negation and disjunction in logic programs through integrity constraints

Integrity constraints were initially defined to verify the correctness of the data that is stored in a database. They were used to restrict the modifications that can be applied to a database. However, there are many other applications in which integrity constraints can play an important role. For example, the semantic query optimization method developed by Chakravarthy, Grant, and Minker for definite deductive databases uses integrity constraints during query processing to prevent the exploration of search space that is bound to fail. In this paper, we generalize the semantic query optimization method to apply to negated atoms. The generalized method is referred to assemantic compilation. This exploration has led to two significant results. First, semantic compilation provides an alternative search space for negative query literals. The alternative search space can find answers in cases for which negation-as-finite-failure and constructive negation cannot. Second, we show how semantic compilation can be used to transform a disjunctive database with or without functions and denial constraints without negation into a new disjunctive database that complies with the integrity constraints.     

基于时态逻辑的自动信任协商模型*

通过分析自动信任协商系统中的行为抽象,形式化定义了协商模式.基于扩展的一阶时态逻辑给出了自动信任协商系统的抽象模型,分析了模型的语法和语义,为实现自动信任协商系统提供了有效的工具.     

线性时序逻辑约束下的滚动时域控制路径规划

针对有限确定性系统中的路径规划问题,本文提出了一种线性时序逻辑约束下的在线实时求解滚动时域控制的新方法。该方法将滚动时域控制方法和满足线性时序逻辑公式的策略相结合,控制目标是在满足高级别任务规范的同时,使收集的累积回报值最大化。其中,在有限时域内的每个时间步长上局部优化回报值,并应用当前时刻计算获得的最优控制序列。通过执行适当的约束,保证控制器产生的无限轨迹满足期望的时序逻辑公式。而且,由于地势影响因子的引入,所建议的方案更接近于真实情况。仿真实验结果验证了文中提出方法的可行性和有效性。     

Applying temporal constraints to the dynamic stereo problem

An algorithm is presented for the problem of the stereopsis of time-varuing images (the dynamic stereo problem). Dynamic stereopsis is the integration of two problems; static stereopsis and temporal correspondence. Rather than finding the intersection of these problems to be more difficult, it was found that by solving the two problem simultaneously, and thus incorporating the spatio-temporal context within which a scene exists, some of the hard subproblems belonging to stereopsis and temporal correspondence could be avoided. The algorithm relies on a general smoothness assumption to assign both disparity and temporal matches. A simple model of the motion of three-dimensional features is used to guide the matching process and to identify conditional matches which violate a general smoothness assumption. A spatial proximity rule is used to further restrict possible matches. The algorithm has been tested on both synthetic and real input sequences. Input sequences were chosen from three-dimensional moving light displays and from “real” grey-level digitized images.     

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.     

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.     

基于行为时序逻辑的入侵取证研究

提出一种基于行为时序逻辑的入侵取证的形式化方法,其描述语言能够准确描述入侵证据、系统知识以及攻击行为,并具有在部分数据缺失的情况下进行非确定性推理的能力;其自动验证工具能够寻求额外的证据并可检查是否有可能的攻击与这些证据相符。实例研究表明,这种方法不依赖于具体的攻击技术和操作系统,不惧证据的缺失,能够有效搜寻更多的证据并重建可能的攻击场景。     

基于行为逻辑的时序使用控制模型

着眼于单主体访问操作中的原子行为和时序性质,采用时序模态逻辑,提出一种基于行为的时序使用控制模型.该逻辑框架包含了与授权相关的按时间节点预定义的行为、由主客体属性和系统所表达的状态序列及状态谓词.在给出了一种策略语言后,对其语法和语义进行了形式定义,并根据使用控制(UCON)模型族的行为特性给出了控制策略.该逻辑模型不仅可以形式化描述使用控制基本原理,而且有助于准确并自动化地判定策略的可满足性,具有良好的灵活性和表达能力.     

Tableau-based automata construction for dynamic linear time temporal logic*

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.*This research has been partially supported by the project MIUR PRIN 2005 ‘Specification and verification of agent interaction protocols’.     

带测试动作的动态时序逻辑扩展

作为一种动态知识表示形式,动态时序逻辑(DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制。为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为2O(n)的证明。分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值。     

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

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

基于时序描述逻辑的Web服务本体语言过程模型语义

针对Web服务本体语言(OWL-S)过程模型存在动态交互和时序特征表达能力不足的问题,提出一种基于时序描述逻辑的过程模型形式化方法。通过对OWL-S过程模型的原子过程和组合过程语义进行形式化的描述,得到了OWL-S的过程模型的动态语义,最终实现了对OWL-S过程模型的形式化建模。实例结果验证了所提方法的可行性,为进一步的分析和验证提供了基础。     

一种基于投影时序逻辑模型检测的入侵检测方法

基于时序逻辑模型检测的入侵检测技术降低了误用检测的漏报率,然而却几乎不能描述并发攻击和分段攻击,因而对这些复杂的攻击模式漏报率仍很高。本文针对该问题,提出了一种基于投影时序逻辑模型检测的入侵检测方法。对若干复杂攻击实例的检测表明,新方法可有效降低对并发攻击和分段攻击的漏报率。     

一种采用一阶动态逻辑表示的数字权限描述模型

针对已有数字权限描述模型的动态语义描述能力较弱问题,提出了一个能够描述权限动 作状态的数字产品权限描述模型DDRM。基于一阶动态逻辑,定义了一个用于描述数字权限概念的 一阶动态逻辑符号系统DrFDL,并在DDRM模型基础上给出了DrFDL的语义结构(该语义结构能够 反映动作的动态特性)。基于DDRM模型还给出了一个表达权限证书的文法,应用DrFDL逻辑语言 给出了该文法生成的权限证书的形式语义,并探讨了该证书的确定性和有效性。     

Persistent surveillance for unmanned aerial vehicles subject to charging and temporal logic constraints

In this work, we present a novel method for automating persistent surveillance missions involving multiple vehicles. Automata-based techniques are used to generate collision-free motion plans for a team of vehicles to satisfy a temporal logic specification. Vector fields are created for use with a differential flatness-based controller, allowing vehicle flight and deployment to be fully automated according to the motion plans. The use of charging platforms with the vehicles allows for truly persistent missions. Experiments were performed with two quadrotors for two different missions over 50 runs each to validate the theoretical results.     

Checking enforcement of integrity constraints in database applications based on code patterns

Integrity constraints (including key, referential and domain constraints) are unique features of database applications. Integrity constraints are crucial for ensuring accuracy and consistency of data in a database. It is important to perform integrity constraint enforcement (ICE) at the application level to reduce the risk of database corruption. We have conducted an empirical analysis of open-source PHP database applications and found that ICE does not receive enough attention in real-world programming practice. We propose an approach for automatic detection of ICE violations at the application level based on identification of code patterns. We define four patterns that characterize the structures of code implementing integrity constraint enforcement. Violations of these patterns indicate the missing of integrity constraint enforcement. Our work contributes to quality improvement of database applications. Our work also demonstrates that it is feasible to effectively identify bugs or problematic code by mining code patterns in a specific domain/application area.