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

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

一种基于有限精度时间自动机的模型检测工具

基于有限精度时间自动机模型,实现了一种新的数据结构——SDS ,用SDS 符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。     

时间自动机可达性分析算法的改进

模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。     

对时间自动机进行空性检测的过程和改进

为了提高对时间自动机进行空性检测的效率,研究了使用基于时钟区域(zone)的符号化方法和抽象对时间自动机进行空性检测,提出了针对时间自动机自身特点对检测过程进行改进的方法.通过使用基于zone的符号化表示方法和抽象,一个符号化状态表示显式的状态的集合,时间自动机的状态空间会显著缩小,不同的抽象方法对状态空间有不同的效果.符号化状态间不仅有相等关系还有包含关系,通过判断这种包含关系可以尽早的找到接收路径和避免不必要的状态展开从而提高空性检测的效率.实现了改进的检测过程,对一些例子进行了数据比较,取得了较好的实验结果.     

利用有限自动机所识别的语言构造petri网的可达性树

可达性树（reachabilty tree）表示petri网的可达标识集。它既和petri网的结构有关，也和petri网的初始标识有关。通过分析petri网的可迭树，可以了解petri网的许多重要性质。因此如何从给出的petri网图转换成奇达性树，是进一步研究petri网的关键。基于此，本文利用有限自动机所识别的语言给出了一种构造petri网可达性树的方法。     

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

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

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

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

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

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

基于扩展RED图的概率时间自动机可达性分析

RED图可以表示一个完整的时间自动机上的状态集,包括其连续时间部分和离散部分.在它基础上实现的模型检测工具RED,在时间自动机模型检测中表现出了优良的性能.另一方面,现有的概率时间自动机模型检测工具仍然使用不同的方法来分别表示概率时间自动机状态的连续时间和离散部分.我们在复用原始RED图的数据结构的基础上,对其做出了扩展,以令其支持概率状态的表达,同时保持其性能方面的优势.我们又为此实现了一个概率时间自动机可达性分析工具原型,并将其与两个概率模型检测工具（PRISM和Modest）就概率时间自动机可达性分析作实验对比,来评估该工具原型的性能.实验结果显示,我们的集成表示概率状态空间的方式,确实提高了概率时间自动机模型检测的时间效率和延展性.     

时间自动机可达性分析中的状态空间约减技术综述

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可迭性分析所需的存储空间,以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向。     

模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.     

Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

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

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

一种基于时间自动机的实时系统模型检查算法的设计与实现

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用Visual C++语言描述了实时特性验证中的数据结构,实现了实时特性验证算法,实验表明利用该算法可以进行实时系统的形式化验证。     

How to Verify a Safe Real-Time System: The Application of Model Checking and Timed Automata to the Production Cell Case Study*

The formal verification of a real-time system requires either a proof theoretic or model theoretic approach. Both being applicable to a model of the proposed behavior of the concurrent real-time system. This paper evaluates the use model checking and timed automata by their application to an adaptation of the Production Cell case study. The Uppaal tool is used in this evaluation. The modeling aspects were found to be straightforward, but to accomplish the necessary model checking required some knowledge of the underlying process. Nevertheless, the conclusion of the study is that these techniques are generally applicable and be can be undertaken in an engineering context without detailed domain knowledge of the model checking technique.     

基于时间自动机的信息物理融合系统建模与验证

信息物理融合系统的建模和验证是当前研究的一个热点。本文通过分析信息物理融合系统的体系结构,利用时间自动机为建模工具,将该结构中的各个组件分别进行建模,以表现它们的分布性和实时性。这些时间自动机组成一个网络模型,用于刻划整个系统之间的并发通信和协作过程。最后,提出一组该系统要满足的性质(包括时间约束),运用模型检测工具UPPAAL自动验证本系统的正确性。     

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

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

Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking

Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and space-efficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficiency of reachability analysis.