STGA的变种及其互模拟验证

为刻画和验证无穷值域上的传值进程,Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型,并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题,该文首先引入了ＳＴＧＡ的一个变种,它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒,因而可定义些种ＳＴＧＡ结果间的符号双迁移关系．文中提出了从正     

面向传值进程的谓词μ-演算与FO(HML)的完备推演系统

作者提出一个谓词μ－演算系统,目的在于描述传值进程的性质,该系统的公式和谓词相互递归定义,谓词中含有抽象式,谓词变元以及最大和最小不动点,其语义模型是带赋值的符号迁移图所诱导的迁移系统,并且该系统包含Hennessy-Milner逻辑的一阶扩弃FO（HML）作为子系统,作者用例说明了本演算系统在表达传值进程性质方面的优越性,该文后半部分主要给出了FO（HML）的一个推演系统,并运用判定树（Tableau)的方法,证明了所给出了推演系统是完备的。     

基于符号迁移图的互模拟验证算法

符号迁移图是传值进程的一种直观而简洁的语义表示模型,该模型由Hennessy和Lin首先提出,随后又被Lin推广至带赋值的符号迁移图,本文不但定义了符号迁移图各种版本（基／符号）的强操作语义和强互模拟,提出了相互的强互模拟算法,而且通过引入符号观察图和符号同余图,给出了其弱互模拟等价和观察同余的验证算法,给出并证明了了τ－循环和τ－边消去定理,在应用任何弱互模拟观察同余验证算法之前,均可利用这些定理对所给符号迁移图进行化简。     

传值进程模型检测中诊断信息的生成

诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义,讨论了传值进程模型检测中诊断信息的生成问题,引入了两种诊断信息的表示结构：证明图和示例;提出了两种诊断信息的构造算法,所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量,相应的算法已经实现并用实例作了分析测试,实验结果表明该方法是有效的。     

移动界程模型检测

首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中,提出了第1个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法,这也是目前已知的第2个带递归的谓词界程逻辑模型检测算法.所做的工作有：①讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性,给出了谓词界程逻辑公式转换成嵌套谓词等式系的方法;②讨论了谓词界程逻辑模型检测问题,给出了具体算法,并分析了算法的复杂性.     

谓词μ演算和模态图的语义一致性

模态图是谓词μ演算的一种有效的图形表示形式.证明了谓词μ演算和模态图的语义一致性,详细讨论了谓词μ演算公式、嵌套谓词等式系和模态图之间的关系,并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法.     

面向实时传值系统的局部模型检测

为对实时传值系统进行模型检测，本文给出了时间符号迁移图作为系统的建模语言，以及实时谓词μ演算作为刻画性质的逻辑语言。本文给出了基于时间符号迁移图和实时谓词μ演算的一个模型检测算法，该算法动态生成和检测可达的状态空间，并且采用对数据变量on—the—fly实例化以及动态切分时间计值集合的方法，是一个局部算法。该算法不仅能处理基于有限域的变量，还可处理一类数据域无穷的变量(称“数据无关”变量)。     

带赋值符号迁移图的局部优化算法

带赋值符号迁移图（ＳＴＧＡ）是刻画一般传值进程的抽象计算模型,在ＳＴＧＡ上可以用“ｏｎ－ｔｈｅ－ｆｌｙ”实例化算法来验证传值进程之间的互模拟等价。由于ＳＴＧＡＡ的一个结点对应于具体迁移图的许多结点,在ＳＴＧＡ上所作的优化对提高互模拟判定算法的时间和空间效率会产生很大的影响。     

数据结构实验的三层模型

分析数据结构实验的特点和难点,借鉴软件工程的多层模型架构,提出数据结构实验设计的三层模型。     

基于约束依赖图的并发程序模型检测工具

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.     

Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems

During the past few years, a number of verification tools have been developed for real-time systems in the framework of timed automata. One of the major problems in applying these tools to industrial-sized systems is the huge memory-usage for the exploration of the state-space of a network (or product) of timed automata, as the model-checkers must keep information about not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n ³) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on-the-fly reduction technique to minimize the space-usage. Based on static analysis of the control structure of a network of timed automata, we are able to compute a set of symbolic states that cover all the dynamic loops of the network in an on-the-fly searching algorithm, and thus ensure termination in reachability analysis. The two techniques and their combination have been implemented in the tool UPPAAL. Our experimental results demonstrate that the techniques result in truly significant space-reductions: for six examples from the literature, the space saving is between 75% and 94%, and in (nearly) all examples time-performance is improved. Noteworthy is also the observation that the two techniques are completely orthogonal.     

基于模型检测的半结构化数据查询

在Web迅猛发展和半结构化数据急剧膨胀的今天,Web上的半结构化数据查询日益成为信息技术领域一个重要的研究发展方向。现有的半结构化查询语言在查询效率上存在着不足。文章提出了一个将模型检测技术应用到半结构化数据查询的新方法,它通过把数据库看作Kripke状态变迁系统,把查询解释为时序逻辑CTL公式,将查询过程转化为模型对公式的满足问题,通过模型检测过程高效地完成数据查询,从而使查询可以在多项式时间内完成,很好地改善了查询效率。最后,给出了该方法在现有半结构化查询语言Lorel上的应用。     

Model-Checking with Coverability Graphs

We show that several formulas of a temporal logic can be verified using the coverability graph of the underlying system. Of course, the procedure is not capable of verifying all formulae, since already the reachability problem for (unbounded) Petri nets is computationally hard. Thus, the procedure returns true, false, or unknown for a query. The formulae that can be verified cover most of the well known standard properties which have been listed in the context of coverability graph analysis so far.     

A Simple and Non-Trivial Ramsey Test

Journal of Logic, Language and Information - This paper expounds a simple and non-trivial Ramsey Test. Drawing on the work of Peter Gärdenfors, it aims to help establish an epistemic...     

一种半自动化异构数据集成工具

论文介绍了用于完成异构数据源数据转换和集成任务的原型系统SDE。该系统以模式映射为基本设计思想,通过本地网关完成异构模式下的查询要求与结果数据的动态转换,并保证结果数据满足目标模式结构与参照完整性的要求。该工具为实现异构系统之间的数据互操作提供了一种有效的解决方案。     

A General Model for Authenticated Data Structures

Query answers from on-line databases can easily be corrupted by hackers or malicious database publishers. Thus it is important to provide mechanisms which allow clients to trust the results from on-line queries. Authentic publication allows untrusted publishers to answer securely queries from clients on behalf of trusted off-line data owners. Publishers validate answers using hard-to-forge verification objects VOs), which clients can check efficiently. This approach provides greater scalability, by making it easy to add more publishers, and better security, since on-line publishers do not need to be trusted. To make authentic publication attractive, it is important for the VOs to be small, efficient to compute, and efficient to verify. This has lead researchers to develop independently several different schemes for efficient VO computation based on specific data structures. Our goal is to develop a unifying framework for these disparate results, leading to a generalized security result. In this paper we characterize a broad class of data structures which we call Search DAGs, and we develop a generalized algorithm for the construction of VOs for Search DAGs. We prove that the VOs thus constructed are secure, and that they are efficient to compute and verify. We demonstrate how this approach easily captures existing work on simple structures such as binary trees, multi-dimensional range trees, tries, and skip lists. Once these are shown to be Search DAGs, the requisite security and efficiency results immediately follow from our general theorems. Going further, we also use Search DAGs to produce and prove the security of authenticated versions of two complex data models for efficient multi-dimensional range searches. This allows efficient VOs to be computed (size O(log N + T)) for typical one- and two-dimensional range queries, where the query answer is of size T and the database is of size N. We also show I/O-efficient schemes to construct the VOs. For a system with disk blocks of size B, we answer one-dimensional and three-sided range queries and compute the VOs with O(log_B N + T/B) I/O operations using linear size data structures.     

Bounded Model Checking with Parametric Data Structures

Bounded Model Checking (BMC) is a successful refutation method to detect errors in not only circuits and other binary systems but also in systems with more complex domains like timed automata or linear hybrid automata. Counterexamples of a fixed length are described by formulas in a decidable logic, and checked for satisfiability by a suitable solver.In an earlier paper we analyzed how BMC of linear hybrid automata can be accelerated already by appropriate encoding of counterexamples as formulas and by selective conflict learning. In this paper we introduce parametric datatypes for the internal solver structure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver.     

Toward Automation for Model-Checking Requirements Specifications with Numeric Constraints

Model-checking techniques have not been effective in important classes of software systems – systems characterised by large (or infinite) input domains with interrelated linear and non-linear constraints over the system variables. Various model abstraction techniques have been proposed to address this problem, but their effectiveness in practice is limited by two factors: first, the abstraction process is manual and requires a great deal of ingenuity; and, second, the abstraction may be coarse and introduce too many spurious behaviours to provide meaningful analysis results. In this paper, we wish to propose domain reduction abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction tech niques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint free and deterministic constrained data transition systems. Our technique is automatable with some minor restrictions. We provide formal proofs for the theoretical soundness of the technique, algorithms for automation, and an illustration of the approach with examples. Correspondence and offprint requests to: Mats P. E. Heimdahl, Department of Computer Science and Engineering, University of Minnesota, 200 Union Street SE, 4-192 Minneapolis, MN 55455, USA. E-mail: heimdahl@cs.umn.edu     

Gambit: An Interactive Database Design Tool for Data Structures, Integrity Constraints, and Transactions

The design of a database is a rather complex and dynamic process that requires comprehensive knowledge and experience. There exist many manual design tools and techniques, but the step from a schema to an implementation is still a delicate subject. The interactive database design tool Gambit supports the whole process in an optimal way. It is based on an extended relational-entity relationship model. The designer is assisted in outlining and describing data structures and consistency preserving update transactions. The constraints are formulated using the database programming language Modula/R which is based upon first-order predicate calculus. The update transactions are generated automatically as Modula/R programs and include all defined integrity constraints. They are collected in so-called data modules that represent the only interface to the database apart from read operations. The prototype facility of Gambit allows the designer to test the design of the database. The results can be used as feedback leading to an improvement of the conceptual schema and the transactions.