UML Statecharts的切片模型检验方法

统一建模语言UML已被广泛应用于软件设计和开发中,而验证UML模型是否满足关键的性质需求成为一个重要问题.由于空间爆炸和语义的复杂性,对Statecharts进行模型检验受到软件规模和设计精化程度的制约.本文在用扩展层次自动机(EHA)结构化的表示UML Statecharts后,通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系.对于由状态和迁移组成的切片准则,给出对EHA进行切片的算法.该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性,且删除了与被验证性质无关的层次和并发状态,缓解了空间爆炸问题.     

UML Statecharts的切片模型检验方法

统一建模语言UML已被广泛应用于软件设计和开发中，而验证UML模型是否满足关键的性质需求成为一个重要问题。由于空间爆炸和语义的复杂性，对Statecharts进行模型检验受到软件规模和设计精化程度的制约。本文在用扩展层次自动机（EHA）结构化的表示UML Statecharts后，通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系。对于由状态和迁移组成的切片准则，给出对EHA进行切片的算法。该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性，且删除了与被验证性质无关的层次和并发状态，缓解了空间爆炸问题。     

基于xUML的模型一致性问题研究

xUML是一种统一建模语言UML的扩展语言,可用于实现自动代码生成。针对xUML代码生成过程中出现的模型不一致问题,文中提出了一种基于xUML类图和活动图的模型完整性和一致性校验方法。首先给出了模型完整性和一致性的校验规则,其次给出了基于规则伪代码形式的算法描述,最后利用工具结合一个具体的实例对完整性和一致性检验算法进行验证。实验结果表明,该方法可以用于对类图和活动图的完整性和一致性验证。     

一种UML2．0模型动态特性的一致性验证方法

近年来，UML已经被广泛应用于软件的分析和设计，然而，由于软件系统的复杂性，在UML模型中，难免会引入不同图表间特别是动态视图之间的不一致性。提出了一种用于验证UML2．0模型状态图和顺序图一致性的方法。首先，用XYZ／E来形式化描述状态图并将其转化为Promela输入语言；然后，用LTL来表示顺序图间的相互作用；最后利用模型检测工具Spin通过检查Promela描述的状态图是否满足LTL公式来达到检测模型一致性的目的。     

基于模型检测的UML状态图和顺序图一致性检测

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,会导致视图不一致的问题。文中提出形式化与可视化UML互补建模的方法,探讨用模型检测验证UML模型中的状态图和顺序图的一致性问题。针对具有复合片段的顺序图提出分析方法,将复杂层次结构的状态图转换为有限状态机,再用模型检测工具NuSMV对建立的模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。     

一种复杂系统定性模型描述方法

复杂系统日益呈现出不确定性、非线性等定性特征,已有的建模方法不足以构建具有定性特征的复杂系统。基于此,提出一种复杂系统定性模型描述方法(QMDM)。QMDM结合定性仿真理论,在UML基础上对其组件图、时序图以及状态图进行扩展,可视化地表达出定性模型的建模过程。组件图用于静态的表达出定性模型包含的定性约束关系。时序图和状态图用于动态的表达出定性模型的时序性,以及状态迁移。此外,给出QMDM的形式化定义,便于以后模型验证,并将研究成果在空调制冷系统中进行了初步应用。     

构件化嵌入式软件设计模型验证工具的研究

基于模型设计与分析技术能够明显提高现代复杂嵌入式软件系统的可靠性,本文基于接口自动机模型设计实现了一个构件化嵌入式软件验证工具并进行了形式化验证。该工具的系统规约采用UML顺序图模型实现,能够对系统设计模型与场景式规约之间多种行为的一致性进行检验,并对实时接口自动机网络与具有时间约束顺序图模型的一致性行为进行检验。     

从UML状态图到PVS规范的自动转换、验证

将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言,具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用.PVS来对UML进行形式化的优势,并且给出了UML的状态图到PVS规范的转换模型与规则.     

基于UML的嵌入式系统模型验证技术的研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可,能对复杂嵌入式系统建模,并有很多成功的应用,但UML是一种半形式化语言,存在时间约束描述能力不强和所建模型形式化复杂、验证难度大等问题。针对上述问题,本文提出了采用实时UML对嵌入式系统UML状态图进行建模;然后用状态-约束-事件矩阵方法来对模型进行形式化描述;最后利用SPIN对模型进行验证。该方法解决了UML在嵌入式系统建模和形式化验证过程中出现的问题,应用实例和结果证明了该方法的有效性和可行性。     

UML状态机到B形式化规约的转换

文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点．将其转换为B形式化模型，然后在B工具环境中遵循B方法的精化原则和正确性验证方法，开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则，涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明．这套转换规则行之有效。     

Efficient test case generation for validation of UML activity diagrams

Unified Modeling Language (UML) is widely used as a system level specification language in embedded system design. Due to the increasing complexity of embedded systems, the analysis and validation of UML specifications is becoming a challenge. UML activity diagram is promising to modeling the overall system behavior. However, lack of techniques for automated test case generation is one major bottleneck in the UML activity diagram validation. This article presents a methodology for automatically generating test cases based on various model checking techniques. It makes three primary contributions: First, we propose coverage-driven mapping rules that can automatically translate activity diagram to formal models. Next, we present a procedure for automatic property generation according to error models. Finally, we apply various model checking based test case generation techniques to enable efficient test case generation. Our experimental results demonstrate that our approach can reduce the validation effort drastically by reducing both test case generation time and required number of test cases to achieve a functional coverage goal.     

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

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

基于进化策略生成可解释性模糊系统

模糊系统的可解释性明显优于其他人工智能方法,却长期没有引起人们足够的注意.本文对模糊系统的可解释性作了深入的分析,定义了最简约模糊划分、模糊划分的完备-清晰性、模糊规则的完备性、紧凑性和一致性,并将其加入到进化策略的适值函数中,用于优化模糊系统.仿真试验表明,即使在先验知识较少的情况下,该方法依然可以设计出具有较好系统响应性能和较高可解释性的模糊系统.     

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

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

基于覆盖率分析的僵尸网络控制命令发掘方法简

从僵尸程序执行轨迹对二进制代码块的覆盖规律出发,提出了一种僵尸网络控制命令发掘方法。通过分析执行轨迹对代码块的覆盖率特征实现对僵尸网络控制命令空间的发掘,根据代码空间是否被全覆盖来验证发现的僵尸网络命令空间的全面性。对僵尸网络Zeus、SdBot、AgoBot的执行轨迹进行了代码块覆盖率分析,结果表明,该方法能够快速准确地发掘出僵尸网络的控制命令集合,时间和空间开销小,且该命令集合所对应的执行轨迹可以覆盖僵尸程序95%以上的代码空间。     

信息系统安全策略研究

安全策略是信息系统安全的关键.信息系统安全的前提是确保安全策略的完备、正确和一致.安全策略的复杂性与系统本身的复杂程度密切相关.安全策略必须得到有效的实施.本文对安全策略的实施、要求和一致性进行了研究,给出了访问控制策略的一致性定理和一致性检查方法.     

Exploiting UML based validation for compliance checking of TLM 2 based models

SoC system designers commonly employ SystemC based Transaction level modeling (TLM) for its early software development usage and its analysis capabilities. TLM helps in realizing a SoC using virtual prototyping by integration of SoC components at different abstraction levels. The TLM 2 standard introduces interoperability rules for the models that may have been developed independently. However, neither SystemC compiler nor TLM library supports checking of such rules and manually debugging interoperability errors in such models could be a major problem. This provides motivation for developing automatic compliance checking techniques which can detect and report such errors. As the models are refined to incorporate detailed intercommunication protocols among the system components, the need for compliance checking extends to these protocols as well. In this paper, we present an efficient UML based compliance checking technique for TLM 2 models which supports static, dynamic and protocol-specific rule checking.