UML状态机的模型检验方法

模型检验是一种确保设计规范正确性的形式化自动验证技术,本文提出了对UML状态机进行模型检验的方法。文中首先对UML状态机的语法和语义进行描述,然后基于语义中的RTC步给出生状态机全局可达状态迁移图的方法,方法的核心是在当前格局下根据使能条件确定所有的最大无冲突迁移集。文章最后给出算法以验证UML状态机是否满足用计算树逻辑（CTL）公式表示的性质。     

AHB片上系统总线的建模与验证

如何有效的对SoC设计进行验证已经成为缩短设计周期的关键问题.针对这个问题,本文提出一种形式化建模与验证方法,对片上系统AMBA工业总线规范的AHB总线协议进行形式化规格;建立了与AHB协议规格对应的有限状态机和SMV模型,使用CTL描述了仲裁器的公平性、从单元活性、从单元的交互操作性、互斥性和无饥饿属性;采用SMV模型检验器对AHB总线协议模型的无饥饿属性进行了自动化验证.结果表明所提方法能够有效应用于SoC的验证.     

无线认证协议Linear MAKEP的模型检验

模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验。对检验结果进行分析发现：在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性。给出了协议的一种改进,使其满足认证性。     

一种系统安全性的形式化验证方法

随着计算机系统应用的深入和广泛,系统安全性越来越成为人们关注的焦点,形式化模型检验是解决系统特性验证问题的一种有效途径,用有限自动机表示系统的设计和实现,用计算树逻辑CTL(ComputationalTreeLogic)公式表示系统的安全特性,探讨了系统安全性形式化验证的方法。     

一种安全协议的机器证明算法

安全协议的形式化验证是网络安全的一个重要领域。文章介绍了一种机器的自动证明算法。与传统算法不同,文章的算法是证伪的从“攻击者”的角度出发,避免了“有限状态机”方法的复杂“状态空间”的搜索。     

基于事件图的离散事件仿真模型并行检验方法

非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.     

基于FSM的协议形式化技术研究

本文主要讨论基于有限状态机(FSM)的协议形式化技术问题。文中论述了FSM形式描述与验证的技术特征,提出了一种增强FSM形式化方法,并给出了基于该方法的形式描述与验证的协议实例。     

基于UML的计算机联锁软件的分析与建模

有效地测试、分析和验证计算机联锁软件是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。以联锁软件的UML非形式化模型为基础,以有限状态机模型为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为有限状态机模型的方法。首先将场景的UML顺序图转化为FSP进程代数模型,然后通过合并不同对象的进程代数模型,得到系统的有限状态机模型。最后以接车进路用例为例生成系统的有限状态机模型,以验证该方法的可行性和有效性。     

SoC有限状态机优化验证方法研究

利用图论及数学规划方法分析并解决有限状态机验证路径的选择优化,提出一种在仿真验证方法中对SOC有限状态机验证路径进行优化的方法．在C＊Core提供的验证环境中,对其部分Golden File验证任务的有限状态机进行了优化处理,通过原方案的验证时间的对比,表明了该方法可以使用更短的时间有效解决有限状态机验证问题．     

基于SMV的网络协议形式化分析与验证

提出了采用模型检验方法对网络协议进行形式化分析及自动验证,建立了一个特定网络协议PAR的有限状态机模型,并用模型检验工具SMV验证其正确性,发现了该协议存在的一些缺陷。结果表明,利用符号模型检验方法分析检验网络协议是可行的。     

基于rCOS的UML状态图语义研究

统一建模语言（UML）中的状态图用于描述类的对象所有可能的状态及事件发生时状态的转移条件,从而进行系统动态分析。针对现有关于UML状态图形式化语义研究中存在的不足,该文提出基于统一程序设计理论的对象精化演算系统,用于描述UML状态图的形式化语义,给出与类图、序列图的一致性检验,为模型驱动开发提供了可行性。     

Complexity of synthesis of composite service with correctness guarantee

How to compose existing web services automatically and to guarantee the correctness of the design (e.g. temporal constraints specified by temporal logic LTL, CTL or CTL*) is an important and challenging problem in web services. Most existing approaches use the process in conventional software development of design, verification, analysis and correction to guarantee the correctness of composite services, which makes the composition process both complex and time-consuming. In this paper, we focus on the synthesis problem of composite service; that is, for a given set of services and correctness constraint specified by CTL or CTL* formula, a composite service is automatically constructed which guarantees that the correctness is ensured. We prove that the synthesis problem for CTL and CTL* are complete for EXPTIME and 2EXPTIME, respectively. Moreover, for the case of synthesis failure, we discuss the problem of how to disable outputs of environment (i.e. users or services) reasonably to make synthesis successful, which are also proved complete for EXPTIME and 2EXPTIME for CTL and CTL*, respectively.     

基于形式化规格说明的UML状态图提取

为了辅助软件开发者理解形式化规格说明,提出一种从B方法规格说明中提取UML状态图的方法。通过分析状态信息在规格说明中的表现形式,定义一系列精确的简单状态、状态迁移、复合迁移、分层状态和状态图通信等提取规则。借助状态变量表和状态迁移表,最终实现状态元素和状态关系的提取,并以此构造完整的UML状态图。实验结果验证了方法的正确性及有效性。     

奥运调度问题模型转换及优化研究

本文研究了奥运会调度问题的模型转换和优化. (1)时间区间约束是奥运会调度问题的关键约束, 本文建立了一种时间区间模型语言以描述这个调度问题. (2)奥运会调度问题是一个约束满足问题, 考虑其本质复杂性, 本文通过柔化决赛时间约束将约束满足问题转化为约束优化问题. (3)约束优化模型中, 项由场地约束关联起来, 如果去掉场地约束, 各项则是相互独立的. 因而本文通过松弛场地约束将约束优化问题分解为若干子问题. 全局优化解通过调整拉格朗日乘子获得. (4)为了调整拉格朗日乘子, 本文研究了变直径次梯度投影算法, 此算法不依赖于任何先验知识收敛, 本文给出了收敛效率. 仿真结果说明了算法的收敛性, 显示出变直径次梯度投影算法与简化算法在性能上的差别, 并且表明原约束满足问题的相变现象可以通过变直径次梯度投影算法获得正的对偶值的概率和首次获得正的对偶值的时间来识别.     

基于动态影响网的C2组织COA问题建模

提出了用动态影响网(Dynamic Influence Nets,DINs)对指挥控制(Command and Control,C2)组织行动过程(Course of Actions,COA)问题进行建模的方法。该方法通过引入因果强度参数,替代了传统动态贝叶斯网络中的条件概率表。给出了利用因果强度参数进行概率传播的具体计算方法。结合一个联合作战的仿真算例,验证了该建模方法的优越性和有效性。     

Conceptual modeling of causal map: Object oriented causal map

This study has been started from question “Is there a methodology that can make causal map comprised of causality as a database by using conceptual modeling method?” In this research, causal map is proposed to represent causal relation by using conceptual modeling method. Therefore, we formalize causality as a cognitive rule to allow us to control changes in the decision making environment. Such causality is embedded in the real world (application domain). And, user (decision maker) use to represent set of causality which decision-makers have retrieved from the set of knowledge or experiences in application domain. Such set of causality that decision-makers possess in their know–how and short (long) term memory are usually formalized by causal map. It is verified for users whether this causal map is helpful in solving their problems. By extending the basis of conceptual modeling theory (ontology theory, classification theory, decomposition theory, and semantic network theory), we introduce a concept of causal entity diagram and address why causal map is needed to analyze a specific domain knowledge for given decision problem solving. Finally, object oriented causal map (O2CM) were employed to verify usefulness of causal map for user (decision maker) in this study.     

基于双层模型的维吾尔语突发事件因果关系抽取

针对传统事件因果关系识别覆盖范围小和人工标注代价高等不足,提出了一种基于双层模型的维吾尔语突发事件因果关系抽取方法. 该方法采用分治思想,将因果关系抽取问题转化为对事件序列的两次模式识别标注. 采用Bootstrapping算法,在第一次模式识别时,标注因果关系的语义角色,并将标注的语义角色标签作为新的特征传递给第二层模式识别,用于因果关系边界标注. 该方法用于维吾尔语突发事件显式因果关系的抽取准确率为85.39%,召回率为77.53%,证明了本文提出的方法在维吾尔语主题突发事件因果关系抽取上的有效性和实用性.     

基于限定的规划识别问题求解

该文把McCarthy的限定理论同规划识别结合起来，在限定中研究规划识别问题，证明了在一定的限制下，由观察到的现象求出的最小规划集与对这些现象作限定获得的解集是一样的，以此为基础，文中提出了一种用限定求解规划识别问题的方式，这种方法把Kautz提出的规划识别表示形式做了某些改变，求解的过程中把二阶限定的表示形式转化为一阶形式，这种一阶形式的限定结果可以用逐点限定的方法直接求得，因为利用了逐点限定的这一特点，该文的方法对限定的计算过程中可以用机器自动完成。     

一种新的时段演算及其验证

在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的.     

机会式频谱接入问题基于事件的优化方法

研究机会式频谱接入技术中次用户对可利用频谱进行探测和接入策略的优化问题. 通过引入事件的概念, 将含有可数无限状态的原问题转化为包含有限个事件的决策问题. 从性能灵敏度的角度出发, 分析不同策略下平均传输率的差异, 给出了基于事件策略的性能差分公式. 以此为基础, 通过合理的近似, 设计了基于事件的策略迭代算法. 仿真示例验证了所提出算法的有效性和近似处理的合理性.