有限精度时间自动机的可达性检测

为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.     

一种基于离散时间自动机的LTL性质检测工具

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.     

有限精度时间自动机的时钟表示

简要介绍了有限精度时间自动机（FPTA）的基本概念,重点讨论FPTA状态中时钟的表示。FPTA只记录时钟值的整数部分,而用时钟序的概念来模拟表示时钟值小数部分的大小关系,从而减少生成的状态空间。在FPTA模型中,时钟操作的时空性能主要依赖于时钟序的数据结构和算法。提出了用位矩阵来表示时钟序的数据结构POM（PartialOrder Matrix）。采用该结构的操作算法具有O(n)复杂度,且无需标准化操作;同时,一切操作均可以通过位运算实现,从而大幅度提高时钟操作的时间效率。     

带时间约束的LTL性质的模型检测的实现

针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。     

一种层次式时间自动机模型检测方法

层次式时间自动机在软件系统建模过程中有着重要的应用.由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作.提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行.在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证.结合实时UML状态机图实例,证明了该方法的有效性.     

基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.     

时间自动机的LTL性质模型检测研究

为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略.采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题.与DTSpin等著名的模型检测工具进行了实验比较,取得了较好的实验结果.     

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.     

基于SCC空性检测中状态空间的缩减方法

对Couvreur提出的基于强连通图的空性检测算法进行改进,使基于嵌套的深度优先搜索与基于强连通图搜索算法的优势结合起来,在对基于迁移的扩展(具有多个可接受条件)Büchi自动机进行空性检测过程中,使用一个布尔变量标识一个状态,不仅节省了内存消耗,而且一般情况下的性能明显优于已有的算法,最坏情况等同于Couvreur的算法.同时反例寻找过程等同于基于强连通图的检测算法.     

Compositional SCC Analysis for Language Emptiness

We propose a refinement approach to language emptiness, which is based on the enumeration and the successive refinements of SCCs on over-approximations of the exact system. Our algorithm is compositional: It performs as much computation as possible on the abstract systems, and prunes uninteresting part of the search space as early as possible. It decomposes the state space disjunctively so that each state subset can be checked in isolation to decide language emptiness for the given system. We prove that the strength of an SCC or a set of SCCs decreases monotonically with composition. This allows us to deploy the proper model checking algorithms according to the strength of the SCC at hand. We also propose to use the approximate distance of a fair cycle from the initial states to guide the search. Experimental studies on a set of LTL model checking problems prove the effectiveness of our method. This work was done when the first two authors were in University of Colorado at Boulder. Parts of this work appeared in preliminary form in [38] and [39].     

Checking Temporal Duration Properties of Timed Automata

In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.     

时间自动机状态空间的一个极小化构造方法

对时间自动机的转换系统进行改进,提出了一个状态空间的极小化构造方法。该方法用位置和停留在该位置时的可能时钟值集合来表示状态,以此隐藏因时间流逝而引发的无穷状态,得到了改进的转换系统——时间段转换系统;并通过对转换可能发生时间的分析,去除无效转换;然后使用转换互模拟合并等价状态,实现了状态空间的极小化,有效地避免了状态空间爆炸。     

实时并发系统的PTSL模型检测

随着实时并发系统的软件规模越来越大、复杂性日趋增加,如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质,它不仅包括对系统模型的遍历以及基于图形的分析方法,而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型（CGS）的扩展,在此基础上添加了概率与时间性质,提出了概率时间并发博弈结构（PTCGS）。同时本文还提出了新的逻辑语言-概率时间策略逻辑（PTSL）,它显式地把策略作为一阶逻辑中的对象,从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求,从而提高系统的可靠性。最后,本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。     

多核模型检测工具CTAV的实现与优化

在计算机计算能力大大增强的时代,为了提高对时间自动机进行空性检测的效率,进一步高效利用多核处理器的优势,研究了利用Büchi自动机的多核空性判定算法改造CTAV,使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具,从而提高模型检测的效率.通过对符号化状态之间包含关系的研究,利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开,实现了多核模型检测算法的优化,对比了一些常见模型的验证数据,取得了更好的效果.     

Improved undecidability results on weighted timed automata

In this paper, we strengthen two recent undecidability results about weighted timed automata, an extension of timed automata with cost variables. More precisely, we propose new encodings of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.     

Optimal infinite scheduling for multi-priced timed automata

This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a powerful abstraction technique of which we show that it preserves optimal schedules. This work has been mostly done while visiting CISS at Aalborg University in Denmark and has been supported by CISS and by ACI Cortos, a program of the French Ministry of Research.     

Robust parametric reachability for timed automata

We review the known decidability and undecidability results for reachability in parametric timed automata. Then, we present a new proof of undecidability in dense time for open timed automata that avoids equalities in clock constraints. Our result shows that the undecidability of parametric timed automata does not follow from their ability to specify punctual constraints in a dense time domain.     

Combining search space partition and abstraction for LTL model checking

The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the integration of search space partition and abstraction improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.