一种基于优先级扩展的时间自动机模型中DBM减法算法的改进

本文介绍一种具有优先级扩展的时间自动机模型,并对一种计算DBM减法算法进行改进。这种减法是DBM上操作中的一种,它会产生需要用DBM集来表示的非凸集合。DBM的数量影响符号模型检测的性能,我们的减法算法是有效的,因为它产生的DBM的数量相对于最初算法具有较大程度的约减。DBM减法操作扩展了具有优先级的时间自动机理论,它对对于具有紧急行为的变换描述、死锁检测、时间博弈等问题具有非常重要的作用。     

时间符号迁移图及其互模拟判定

引入时间符号迁移图的概念，作为既涉及通讯又具有实时性的并发系统的模型，该文给出了这种迁移图时间互模拟的算法，并证明了该算法的正确性。     

时间自动机模型验证的研究进展

基于时间自动机的模型验证是一种形式化的实时并发系统时间性质验证技术,重大软件对时间行为、时序关系的高可靠性要求,不断刺激时间自动机模型验证技术的发展.介绍了时间自动机理论、模型验证算法及工具,对该领域的研究进展做了综述,指出了时间自动机模型验证存在的问题和研究方向.     

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

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

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

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

Model Checking Semi-Continuous Time Models Using BDDs

The verification of timed systems is extremely important, but also extremely difficult. Several methods have been proposed to assist in this task, including extensions to symbolic model checking. One possible use of model checking to analyze timed systems is by modeling passage of time as the number of taken transitions and applying quantitative algorithms to determine the timing parameters of the system. The advantage of this method is its simplicity and efficiency. In this paper we extend this technique in two ways. First, we present new quantitative algorithms that are more efficient than their predecessors. The new algorithms determine the number of occurrences of events in all paths between a set of starting states and a set of final states. We then use these algorithms to introduce a new model of time, in which the passage of time is dissociated from the occurrence of events. With this new model it is possible to verify systems that were previously thought to require dense time models. We use the new method to verify two such examples previously analyzed by the HyTech tool: a steam boiler example and a fuel injection controller.     

Language equations for timed alternating finite automata

Traditionally, finite state automata are untimed or asynchronous models of computation in which only the ordering of events, not the time at which events occur, would affect the result of a computation. For real-time systems, it is important to augment these models of computation with a notion of time. For this purpose timed automata have become a powerful canonical model for describing timed behaviors and an effective tool for modeling real-time computations. In this paper, we extend the notion of timed alternating finite automata (TAFA), a class of alternating finite automata (AFA) extended with a finite set of real-valued clocks, and we present an algebraic interpretation of TAFA which parallels that of timed regular expressions and language equations. We further extend the equational representation of AFA to describe timed alternating finite automata, and explore solutions for such equations over time languages.     

Forward Analysis of Updatable Timed Automata

Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it suffers from a state explosion and is thus not used in practice. Instead, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.In this paper, we study in detail this widening operator and the corresponding forward analysis algorithm. This algorithm is most used and implemented in tools like KRONOS and UPPAAL. One of our main results is that it is hopeless to find a forward analysis algorithm for general timed automata, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in detail this algorithm in the more general framework of updatable timed automata, a model which has been introduced as a natural syntactic extension of classical timed automata. We describe subclasses of this model for which a correct widening operator can be found.     

Verifying Automata Specification of Distributed Probabilistic Real-Time Systems

In this paper,a qualitative model checking algorithm for verification of distributed probabilistic real-time systems(DPRS)is presented.The model of DPRS,called real-time proba bilistic process model(RPPM),is over continuous time domain.The properties of DPRS are described by using deterministic timed automata(DTA).The key part in the algorithm is to map continuous time to finite time intervals with flag variables.Compared with the existing algorithms,this algorithm uses more general delay time equivalence classes instead of the unit delay time equivalence classes restricted by event sequence,and avoids generating the equivalence classes of states only due to the passage of time.The result shows that this algorithm is cheaper.