数据关联的时序有限自动机模型的建模方法

介绍了一种用时序自动机为数据关联问题建模的方法，对数据关联问题的研究方法做了新的尝试。目前有多种数据关联算法，对这些方法的分析和评价成为急于解决的问题。鉴于观测信息的时序性，该文以有限自动机(FA)为基础，将时间序列引入到有限自动机中，定义了时序有限自动机(TFA)，建立了数据关联(DA)的时序有限自动机模型，用于判断关联算法得到的航迹准确性。     

基于UPPAAL的数据关联时序有限自动机模型验证

对数据关联过程建立了时序有限自动机模型，时序有限自动机时钟变量只取整数值，从而减小数据关联过程生成的状态空间。在一定的时间约束下，使用模型检测工具UPPAAL对所建模型的关键性质——关联准确性进行了分析和验证。检测结果验证了利用UPPAAL进行数据关联准确性分析的可行性。     

基于事件确定有限自动机的UML2.0 序列图描述与验证

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.     

Mizumoto格值有限自动机及其最小化

提出取值为格半群的Mizumoto格值有限自动机的概念,得到基于模糊字符串的Mizumoto格值有限自动机的扩张模型,并详细讨论了其性质。同时建立了扩张Mizumoto格值有限自动机与标准扩张Mizumoto格值有限自动机的等价性,在此基础上给出了其最小化算法。     

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

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

基于系统调用的入侵检测新方法*

通过分析系统调用行为特征,提出了程序的系统调用行为可以用有限状态自动机来描述的方法,证明了算法产生的自动机的完整性,并给出算法性能分析结果。     

基于矩阵模型表示的有限自动机极小化方法

论文基于有限自动机的矩阵模型犤1犦,并以矩阵理论和布尔代数为工具,给出了一种有限自动机极小化的新方法。该方法不仅有利于算法设计和计算机自动处理,也表明了矩阵模型方法在有限自动机应用研究中的重要作用。     

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

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

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

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

有限自动机在复合事件检测中的应用

针对早期系统只提供原子事件的检测机制,不能检测由原子事件组成的复合事件的问题,提出了用有限自动机来检测复合事件的方法.说明了复合事件的组成和表达式,利用自动机原理对复合事件的检测模式进行了分析,给出了复合事件检测的具体过程:从事件表达式到不确定的有限自动机,从不确定的有限自动机到最小化确定的有限自动机,再用程序实现了确定的有限自动机.实例表明,自动机模型是检测复合事件的一种有效实现方式.     

OWL-S过程模型的形式化描述与相容性分析

构建组合服务的形式化模型是对其进行验证的前提与基础,然而缺乏统一的构建框架使得建模过程变得难以把握且无法实现自动化。通过对确定型有限自动机的扩展,建立了用于描述OWL-S过程模型的有限迁移系统——服务过程自动机,为组合服务的形式化建模提供了统一框架和自动化基础。同时,通过分析服务过程自动机的可接受位置及其在组合过程中可能产生的约束,将相容性划分为三个等级,从而能够在不同强度的可靠性要求下进行组合服务的验证工作。     

右线性文法与有限自动机等价性的一个新证明

迄今为止,左、右线性文法与有限自动机的等价性都是通过相互模拟构造来证明的。文章首先引入字母表上的右线性方程组及其最小解的概念,证明了最小解的存在性与有效可解性,描述了最小解的结构;其次通过右线性方程组及其最小解,证明了右线性文法与有限自动机的等价性。完全类似地,可以引入字母表上的左线性方程组及其最小解,并且证明左线性文...     

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.     

On transformations of formal power series

Formal power series are an extension of formal languages. Recognizable formal power series can be captured by the so-called weighted finite automata, generalizing finite state machines. In this paper, motivated by codings of formal languages, we introduce and investigate two types of transformations for formal power series. We characterize when these transformations preserve recognizability, generalizing the recent results of Zhang [16] to the formal power series setting. We show, for example, that the “square-root” operation, while preserving regularity for formal languages, preserves recognizability for formal power series when the underlying semiring is commutative or locally finite, but not in general.     

Formal power series and regular operations on fuzzy languages

In this paper we study formal power series over a quantale with coefficients in the algebra of all languages over a given alphabet, and representation of fuzzy languages by these formal power series. This representation generalizes the well-known representation of fuzzy languages by their cut and kernel languages. We show that regular operations on fuzzy languages can be represented by regular operations on power series which are defined by means of operations on ordinary languages. We use power series in study of fuzzy languages which are recognized by fuzzy finite automata and deterministic finite automata, and we study closure properties of the set of polynomials and the set of polynomials with regular coefficients under regular operations on power series.     

Weighted tree automata and weighted logics

We define a weighted monadic second order logic for trees where the weights are taken from a commutative semiring. We prove that a restricted version of this logic characterizes the class of formal tree series which are accepted by weighted bottom-up finite state tree automata. The restriction on the logic can be dropped if additionally the semiring is locally finite. This generalizes corresponding classical results of Thatcher, Wright, and Doner for tree languages and it extends recent results of Droste and Gastin [Weighted automata and weighted logics, in: Automata, Languages and Programming—32nd International Colloquium, ICALP 2005, Lisbon, Portugal, 2005, Proceedings, Lecture Notes in Computer Science, Vol. 3580, Springer, Berlin, 2005, pp. 513–525, full version in Theoretical Computer Science, to appear.] from formal power series on words to formal tree series.     

Specification of temporal properties with OCL

The Object Constraint Language (OCL) is widely used to express static constraints on models and object-oriented systems. However, the notion of dynamic constraints, controlling the system behavior over time, has not been natively supported. Such dynamic constraints are necessary to handle temporal and real-time properties of systems.In this paper, we first add a temporal layer to the OCL language, based syntactically on Dwyer et al.'s specification patterns. We enrich it with formal scenario-based semantics and integrate it into the current Eclipse OCL plug-in. Second, we translate, with a compositional approach, OCL temporal properties into finite-state automata and we connect our framework to automatic test generators. This way, we create a bridge linking model driven engineering and usual formal methods.     

基于Uppaal的实时系统AADL数据流模型的转换与验证

体系结构分析设计语言AADL是一种可支持软硬件一体化建模及同一模型多元分析的形式化与图形化建模语言。采用时间自动机形式化模型检验方法对AADL模型中的数据流进行转换和验证。考虑到单一数据流与混合数据流的差异性,分别设计了数据流到时间自动机模型的转换规则,并通过时间自动机网络实现数据流的综合分析。设计开发了自动化模型转换的插件AADLToUppaal Plug-in,将其嵌入到OSTATE工具中,使用时间自动机建模与验证工具Uppaal对转换得到的时间自动机进行模拟和验证,等价地验证所设计的AADL模型数据流时延是否满足系统实时性要求。仿真实验结果表明,所设计的数据流模型转换方法能有效地将AADL模型转换到时间自动机模型,并能在Uppaal中正确地分析原模型的数据流时延特性。