面向模型检验的UML状态机语义

UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图．它丰富的表示符号提供了强大的描述机制，但也降低了其结构的模块性，提高了对其分析验证的难度．模型检验是自动检验有限状态并发系统的技术．通过模型检验SM描述的不同系统元素的行为是否满足某些性质，能尽早发现设计中的错误．为了将模型检验技术应用于SM的验证，本文用kripke结构定义SM的操作语义．与已有的SM语义定义不同，本文考虑到了SM中包含的不确定因素，用kripke结构描述系统所有可能的演化轨迹、通过检验从SM翻译得到的kripke结构达到模型检验SM的目的．     

面向方面动态行为建模研究

静态模型和动态模型从不同角度反映了系统的结构与行为.横切关注点的静态模型反映了系统的静态结构,为进一步开发提供了静态视图;动态模型则描述了系统结构元素的动态特性及行为,描绘了参与用例的所有对象之问的交互,通过对象间交互实现系统的功能.由于面向对象系统的动态建模通常由UML交互图表示,所以本文在UML交互图基础上,建立面向方面横切关注点的动态模型.     

基于UML的建模及模型检验研究

UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UUL模型进行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动检验技术。为了检验UML模型的正确性,在建模的基础上把UML模型转换为SMV模型,然后使用符号模型检验器（SMV）对模型进行检验,有利于在系统的设计早期发现系统的缺陷。     

面向方面动态行为建模研究

静态模型和动态模型从不同角度反映了系统的结构与行为。横切关注点的静态模型反映了系统的静态结构,为进一步开发提供了静态视图;动态模型则描述了系统结构元素的动态特性及行为,描绘了参与用例的所有对象之间的交互,通过对象问交互实现系统的功能。由于面向对象系统的动态建模通常由UML交互图表示,所以本文在UML交互图基础上,建立面向方面横切关注点的动态模型。     

UML到Verilog同态映射在SOC系统级建模上的应用

SOC设计变得日益复杂要求我们在更高层次抽象上分析和验证系统行为。更精细的系统级建模方法变得日趋重要。文章主要目标是阐述怎样使用统一建模语言UML来构建一个复杂SOC设计框架及抽象其各个模块间行为的交互，建立了一个UML到Verilog的同态映射。提出了一个基于同态映射的从UML模型子集自动导出相应可综合Verilog描述的算法，为UML模型对于建模硬件系统提供了形式化的语义，从而能够验证并综合UML模型，加快了SOC设计流程。     

基于MDA的语义Web服务的组合与验证

针对语义组合Web服务的验证问题,研究了模型验证相关技术、统一模型语言(UML),提出了基于模型驱动架构(MDA)的组合方法.该方法使用UML类图和用例图对OWL-S进行静态组合建模,使用活动图对OWL-S进行动态组合建模,实现了语义组合Web服务的UML描述,然后将该描述转换为Promela语言代码,在Promela代码之后增加LTL的声明,使用SPIN工具进行正确性、安全性和活性验证.该模型保证了组合过程的正确性.     

UML类模型的VDM++形式化规约

利用目前使用最为广泛的形式化验证语言VDM++在描述系统模型的语法和语义上的精确、一致的特点,结合VDMTOOLS和Rational Rose工具把UML类模型中的各个元素转化成VDM++表示,从而实现对UML类模型中所包含的各个元素进行语法和语义的检查。进一步提高UML的建模质量。     

基于扩展层次自动机的UML状态图完备性和一致性检验

UML状态图是UML中重要的建模元素之一,用以描述软件系统的离散行为。完备性和一致性是UML状态图模型最重要的性质之一,是进一步验证模型行为正确性的前提。给出了状态图模型完备性和一致性的定义,研究了对完备性和一致性进行检验的方法。该方法首先把状态图模型变换成扩展层次自动机(EHA),然后对EHA进行分析。EHA中间格式消除了状态图的复杂性,简化了冲突迁移的优先级判别,便于设计简捷有效的算法对完备性和一致性进行检验。该方法的主要优点是利用了EHA的特性,给出了组合状态上迁移的传播算法,解决了完备性和一致性分析的难点。     

用例模型的Z语言形式化描述方法

以UML用例模型为主要研究对象,通过对UML用例模型概念和Z抽象符号的分析,采用Z形式化语言对用例模型建模元素的抽象语法和语义进行形式化的描述,提出了用例模型到Z形式语言的映射规约,并建立了UML用例模型图到Z形式规约的映射与转换机制。     

一种面向嵌入式软件体系结构的形式化建模方法

为了解决MARTE（Modeling and Analysis of Real Time and Embedded systems）在建立嵌入式软件模型时不够精确的问题,结合Object-Z和PTA（Probabilistic Timed Automation）的优点,本文提出了一种集成的形式化建模方法--PTA-OZ.该方法不仅能够对嵌入式软件模型的静态语义和动态语义进行精确描述,而且通过模型转换规则,能够将MARTE模型转换为PTA-OZ模型.并对模型转换的语义一致性进行了验证,证明本文方法在转换过程能够保持结构语义和行为语义的一致性.最后通过实例模型描述从嵌入式软件建模到属性检验的过程.     

浅析模型检测技术

模型检测是一种能够自动验证有限状态并发系统技术.通过显式状态搜索来验证有限状态并发系统的模态与命题性质,当前已被广泛应用于计算机软硬件系统安全性能的检测.本文浅析了模型检测技术,分析了模型检测技术的发展概况、基本原理、算法、模型检测工具等,并介绍了模型检测领域的最新进展.     

基于SPIN的模块化模型检测方法研究

该文针对模型检测过程中所存在的状态爆炸问题,提出了一种基于模型检测工具SPIN的模块化模型检测方法。所提出的方法能够将指定的抽象模型分解成若干的模块,并对这些验证复杂度相对低的模块执行模型检测,以替代对原模型的模型检测。所提方法所用的分解过程保留了原模型所有的语义,同时不增加额外的语义,从而使得验证所有模块等同于验证原模型。理论和实验分析结果显示了所提方法的有效性。     

一种认证协议的检测模型

在分布式系统中,客户向对方证实自己的身份以及建立会话密钥已是非常重要,密码协议的实施就是达到这种目的的有效方法。但密码协议的设计容易出错。本文给出了一种密码协议分析和检测模型,该模型对密码协议的描述简单而且直观。在此模型中,协议被描述成状态变换系统,通过对系统状态的检测,能够发现协议中存在的泄漏。最后,给出了如何将改进的TMN协议模型化,并找出了一种新的攻击,同时,给出了TMN协议的进一步改进。     

Verification of Secure Network Protocols in Uncertain Environments

In this paper, we present a method for protocol checking and verification using discrete event control. By protocol checking and verification, we mean verifying that a protocol is logically correct, that it does not cause deadlocks, and that it has been defined to respond to uncontrollable events that may occur in a system implementing it. Our approach differs from those previously suggested in two key ways. We extend the elementary theory of discrete event control to allow us to model more complicated protocols, including protocols relying on arbitrary counting models. We then present a maximum probability method for analyzing a protocol’s ability to react to a priori unspecified events. Unlike current protocol modeling, we use a pushdown automata for modeling protocols. This allows us to model protocols with greater fidelity. Our methods are illustrated using a simple two-level hierarchical protocol that defines the behavior of ad hoc wireless network nodes as they attempt to establish a secure connection. As wireless networks become more prevalent throughout the world, the off-line verification of protocols before they are implemented will help ensure that wireless network protocols are robust to security intrusions before they are deployed into the field. This will save time and money in the long run.     

SHIM: a deterministic model for heterogeneous embedded systems

Typical embedded hardware/software systems are implemented using a combination of C and an HDL such as Verilog. While each is well-behaved in isolation, combining the two gives a nondeterministic model of computation whose ultimate behavior must be validated through expensive (cycle-accurate) simulation. We propose an alternative for describing such systems. Our software/hardware integration medium (shim) model, effectively Kahn networks with rendezvous communication, provides deterministic concurrency. We present the Tiny-shim language for such systems and its semantics, demonstrate how to implement it in hardware and software, and discuss how it can be used to model a real-world system. By providing a powerful, deterministic formalism for expressing systems, designing systems, and verifying their correctness will become easier.     

A framework for resilient Internet routing protocols

At a fundamental level, all Internet-based applications rely on a dependable packet delivery service provided by the Internet routing infrastructure. However, the Internet is a large-scale complex loosely coupled distributed system made of many imperfect components. Faults of varying-scale and severity occur from time to time. In this paper we survey the research efforts over the years aimed at enhancing the dependability of the routing infrastructure. To provide a comprehensive overview of the various efforts, we first introduce a threat model based on known threats, then sketch out a defense framework, and put each of the existing efforts at appropriate places in the framework based on the faults and attacks against which it can defend. Our analysis shows that although individual defense mechanisms may effectively guard against specific faults, no single fence can counter all faults. Thus, a resilient Internet routing infrastructure calls for integrating techniques from cryptographic protection mechanisms, statistical anomaly detection, protocol syntax checking, and protocol semantics checking to build a multifence defense system.     

具有模糊时态的广义可能性线性时序逻辑的模型检测

本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL（Generalized Possibilistic Fuzzy Linear Tempora Logic）的语构以及基于路径和基于语言的两种语义解释,证明了GPoFLTL在模糊时态方面对GPoLTL（Generalized Possibilistic Linear Tempora Logic）进行了扩张,并通过实例说明了GPoFLTL比GPoLTL具有更强的表达能力;其次在广义可能性测度下通过模糊矩阵运算讨论了"不久","几乎总是"等几类模糊时态性质的模型检测问题;最后研究了模糊时态性质的必要性阈值模型检测问题,给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.     

不确定型模糊Kripke结构的计算树逻辑模型检测

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词∃和任意量词∀在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词∃_sup,∃_inf和∀_sup,∀_inf,分别用于替换存在量词∃和任意量词∀.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式∃_suppUq,∀_suppUq,∃_infpUq和∀_infpUq分别给出时间复杂度为对数多项式时间的改进算法.