确定有穷自动机的最小化问题探讨

本文针对DFA最小化时可能遇到的各种情形,给出最小化的通用算法,并通过具体实例加以验证。此算法有利于学生对编译原理课程中DFA最小化的学习和理解,同时让学生进一步了解此知识点在其他问题求解中的应用。     

有限状态自动机的并行确定化及过程分析

本文通过对并行环境下非确定有限自动机和确定有限自动机的等价性和转换进行研究，详细分析了非确定有限自动机到确定有限自动机的并行转换方法及算法，并以实例给出了其间并行转化的过程。     

UML Statecharts的模型检验方法

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.     

入侵检测系统中模式匹配自动机的构造研究

本文提出了一种新的用于构造入侵检测模式匹配自动机的方法。该方法从构造判定单个模式的NFA自动机入手,通过集成单个的NFA而得到全集的NFA,并将全集NFA转换为与之等价的DFA并化简,从而可得到全集的确定型模式匹配有限自动机。由于该方法可以完全自动完成,从而可以方便地为入侵检测系统构造模式匹配自动机。     

有穷自动机的多媒体教学系统设计

利用多媒体技术的优势,采用多媒体课件制作工具Flash 8.0软件,将图形、动画和影视等多种媒体的素材溶于编译原理课程的教学课件中,形成富有特色的多媒体教学课件;学生通过系统能够进行自主学习,提高对形式语义、有穷自动机等抽象内容的学习兴趣、增强课堂教学效果。设计了该有穷自动机多媒体教学系统,既可在课堂上演示,也可在课后由学生自主观摩,以增强对编译原理课程的学习效果。     

一种基于时间自动机的时钟等价性优化方法

提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机.优化时钟等价规则,在一定程度上有效地解决了状态空间爆炸问题.     

判定非确定离散事件系统稳定性的多项式复杂度算法

本文讨论基于非确定自动机,形式语言模型的非确定离散事件系统稳定性的多项式算法.在引入拟距离的概念之后.根据拟距离形式化地定义了非确定离散事件系统稳定性.以往判定非确定离散事件系统稳定性的算法基于系统的观测器实现,该观测器在结构上具有指数复杂度,因此本文分析系统结构和观测器结构之间的关系,基于对系统状态对的讨论,提出了判定系统稳定性的有效多项式搜索算法.     

判定非确定离散事件系统稳定性的梯度搜索算法

讨论基于非确定自动机/形式语言模型的非确定离散事件系统(NDES)稳定性问题.引入非确定离散事件系统稳定性的定义,并得到了稳定性的判据定理.给出了基于梯度的搜索算法,该算法可有效消除观测器的冗余,从而降低了计算复杂度.     

一种利用非确定规划的LTL合成方法

LTL合成(Linear Temporal Logic synthesis)是程序合成(program synthesis)的一类重要子问题, 旨在自动构建一个控制器(controller), 且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说, 可以将LTL合成定义为二人博弈(two-player game)问题, 博弈的双方是环境和控制器, 该问题的解称为合成策略.近年来, 有研究从理论角度讨论了LTL合成与非确定规划(non-deterministic planning)的相关性.基于此, 本文提出了一种新的利用非确定规划求解LTL合成问题的方法, 并证明了方法的正确性和完备性.具体而言, 首先获得LTL公式对应的Büchi自动机, 结合二人博弈定义, 将LTL合成问题转换为完全可观测的非确定规划模型, 然后交由高效规划器求解.通过实验结果说明, 与其他LTL合成方法相比, 本文提出的基于规划的合成方法在解质量方面具有较大的优势, 能够获得规模较小的合成策略.     

基于子集构造法的优化的NFA确定化算法

使用子集构造法对非确定有限自动机进行确定化的过程中存在大量重复计算的问题.为解决此问题,基于非确定有限自动机的特点并针对子集构造法的不足,提出了一种优化的非确定有限自动机确定化算法.首先定义了识别符的有效引出状态集概念并证明了ε-closure的并定理以保证算法的正确性,其次给出了用于避免重复计算的识别符的有效引出状态集的构造子算法和单状态集的ε-closure的求算子算法,基于这两个子算法给出了优化的非确定有限自动机确定化算法,最后将算法应用于实例,实验结果表明计算量远小于子集构造法的计算量.相比子集构造法,算法能更有效地对非确定有限自动机进行确定化.     

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.     

PSL逻辑及验证技术研究进展与展望*

在简要介绍PSL的分层结构和语法与语义基础上,综述了PSL验证技术的应用研究现状,分析了各种方法、技术的优缺点,最后指出了PSL验证技术的未来研究展望。     

基于PSL断言的宽带电路交换芯片验证

利用基于PSL断言的验证方法验证了宽带电路交换芯片XYDXC160的设计。该芯片单片支持64路2.488Gb/s STM-16帧结构的SDH码流的输入/输出，实现1 024×1 024 STM-1流的无阻塞电路交换。断言技术的引入，降低了验证工作的复杂度，提高了验证的速度和效率，确保了验证工作的质量。     

覆盖率驱动的芯片功能验证设计与实现

随着芯片集成度的发展,芯片性能越来越高,而上市时间越来越短,芯片验证在芯片设计中非常关键并贯穿于整个设计过程,验证的效率和质量直接决定着芯片的成败。提出了基于覆盖率驱动的芯片功能验证方法,定义了基于功能点覆盖率驱动的验证流程,利用PSL语言描述断言检查很有效,通过模拟工具检查断言是否成功,从而判断设计是否满足系统的功能要求。在网络接口芯片实际应用中,有效地降低了验证工作的复杂度,同时提高了验证的速度和质量。利用功能覆盖率数据判断测试激励的正确性和完整性,同时用覆盖率数据定量评价验证进程,提高了整个设计的效率。     

一种接口自动机的组合精化检验方法

接口自动机是一个用来描述软构件接口的时态行为的形式模型，传统的简单组合精化检验规则由于没有考虑到环境时子任务的影响而使其实际应用受到较大限制。本文提出了一种对该规则的改进方法，以弥补上述缺陷。     

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

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用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.     

使用形式化验证方法进行流水线验证

随着流水线技术的广泛应用,流水线设计的验证问题也越来越受到业界的关注.本文提出的方法作为自上而下验证方法的一部分,可以在指令级对流水线设计的正确性进行检验.本文从控制逻辑的角度对流水线的行为进行分析,通过为控制逻辑建立FSM表示,以及采用NuSMV作为验证工具,达到对流水线的自动验证.这种方法的优势在于是以流水段为单位进行检验,这种局部验证的方法不但可以降低建模和检验的复杂度,还可以极大地缩短验证时间.     

UML状态机模型元素的RSL形式化定义

UML状态机作为UML动态描述机制的重要组成部分,在描述系统及模型的动态行为时扮演着重要的角色,但已有的UML动态语义缺乏准确的形式化描述。首先将UML状态机抽象成图;再将图通过传统的有穷自动机进行语义扩展,同时增加状态分层,形成一个基于UML状态机的有穷自动机;然后用RAISE规约语言RSL对扩展后的自动机进行形式化定义,使UML状态机中的模型元素的语义更加清晰、精确,为后期的UML状态机的操作语义形式化研究打下基础。     

一种有效的基于LTL和Petri网的模型检测方法

模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。