共查询到20条相似文献,搜索用时 468 毫秒
1.
2.
面向方面通过分离关注点解决软件系统中的横切问题,通过扩展UML可实现对面向方面的建模。本文利用UML的扩展机制将方面加入状态图中,描述了状态图中的方面与核心组件以及方面之间的编织,然后利用进程代数的形式化语义描述了扩展后的UML状态图,克服了扩展UML描述状态图的缺乏形式化动态语义,不利于对模型进行形式化验证和证明的缺
点。最后,以ATM自动取款机为例验证了基于CSP的面向方面状态图形式化描述的有效性。 相似文献
点。最后,以ATM自动取款机为例验证了基于CSP的面向方面状态图形式化描述的有效性。 相似文献
3.
4.
针对面向对象软件回归测试的新特点,本文引入了基于UML图的不同粒度切片。首先,对描述类间关系的UML类图和描述状态变迁关系的UML状态图形式化定义。接着,对定义的图进行切片分析,其中类间测试提出一种基于UML类图的粗粒度切片工具;类内测试提出一种基于UML状态图细粒度切片的方法。最后,将其应用于销售订单系统,结果表明以上两种分析方法可以有效地提高回归测试效率。 相似文献
5.
标准UML(unified model language)状态图中缺乏对并行环境精确的动态语义,不利于对其所描述的并行环境进行形式化分析、验证和确认,而CSP(通信序列进程)语言具有严格的数学定义和分析方法,可用于验证模型的正确性.针对此特点,提出了结合CSP的UML状态图的形式语义,同时给出在并行环境下UML状态图的... 相似文献
6.
面向对象模型的形式化是形式化研究的重点,UML是一种得到承认的标准建模语言,CHAM是一种广泛用于异步并行计算和系统体系结构建模的语言,它适合对系统的状态变化进行动态的描述.利用和改进原有的CHAM建模语言,使其能够对UML状态图进行形式化描述. 相似文献
7.
本文提出了一种新的定义UML形式化语义的方法。我们将建模语言的语义区分为描述语义和功能语义两个方面。描述语义定义哪些系统满足模型,功能语义定义模型中的基本概念。本文用一阶逻辑定义了UML的类图、交互图和状态图的描述语义,并介绍我们实现的将UML模型转换成逻辑系统的软件工具LAMBDES,该工具集成了定理证明器SPASS,可以对模型进行自动推理。我们成功地将此方法和工具应用于模型的一致性检查。 相似文献
8.
统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器(SPIN)对UML模型进行检测的方法。首先对UML模型进行形式化描述,使用层次自动机来描述状态图,然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA,使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束,通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。 相似文献
9.
基于UML的嵌入式系统模型验证机制的研究 总被引:8,自引:0,他引:8
随着嵌入式系统在各个领域的广泛应用,嵌入式系统变得越来越复杂,研究一种支持嵌入式系统从分析、设计、验证到编码这一整个开发过程的模型系统及建模方法变得越来越重要。UML(UnifiedModelingLanguage,统一建模语言)作为面向对象的分析与设计技术的代表,已经获得了广泛的承认,并在多个领域中有成功的应用。然而,UML是一种符号化语言系统,其语义采用自然语言描述,没有完全形式化,无法精确和严格地描述模型的行为从而实现模型的验证。为了解决这个问题,文章提出了一种用于嵌入式系统UML模型验证的方法,其核心是可执行(Executable)UML,它是UML的增强性子集,采用与UML相同的符号表示法,并集成了状态图(StateChart)所用的形式化语义定义。嵌入式系统的UML模型经过语义分析能够很方便地生成可执行UML模型,并实现系统模型的验证。 相似文献
10.
UML缺乏精确的语义,难以对其所表示的系统进行形式化分析和一致性检验.为了使UML能够更精确地对系统模型进行描述,学者们提出了一些形式化的方法.论文对比分析了用Petri网、时序逻辑XYE/E和动态描述逻辑形式化UML状态图的方法,指出了它们各自的优缺点以及应用领域. 相似文献
11.
在统一建模语言(UML)规范中顺序图的语义是以自然语言的形式描述的,是一种半形式化的语言,不能对系统的交互行为进行形式化分析及论证.针对UML顺序图缺乏精确的形式化描述问题,根据顺序图的时序特征,提出了增加交互操作符的UML顺序图的六元组形式化方法.对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑.应用时序描述逻辑的时态算子得到时序描述逻辑语义形式的UML顺序图.用UML顺序图描述完整的C语言执行过程,将其形式化描述,实验结果表明,这种方法是可行的. 相似文献
12.
UML状态图能有效的表现系统的并发控制和类的嵌套,但用其实现的类测试用例复杂.研究了UML状态图和扩展有限状态机这两种方法在软件测试中状态转换的特点,利用扩展有限状态机状态转换单一线索化的特点降低UML状态图在类测试用例生成中的复杂性.以一个坐标图形显示类的测试用例生成为例,详细讨论了结合扩展有限状态机状态转换特点的UML状态图在面向对象测试技术中的应用. 相似文献
13.
14.
针对当前商业环境中传统企业资源计划(ERP)系统的低开放性、低拓展性和高成本等问题,提出了一种基于软件即服务(SaaS)模式的ERP系统建模方法。首先,利用UML的拓展机制,对原语扩充,得到新的原语集UML profile;其次,建立等效元模型,通过对象约束语言(OCL)保证语义的无二义性;最后,通过应用图、操作字典、物理图和拓扑图组成的模型框架对云ERP系统进行描述,实现云ERP系统的文档化。该方法专注于模块化设计,所有阶段均采用统一的可视化元模型。根据建模需求,在企业架构(EA)平台上采用所提方法成功建立了基于SaaS的云ERP模型,验证了所提建模方法的有效性。理论分析及建模结果表明,该方法确保了模型间的互操作性和一致性,提高了ERP系统的可成长性。 相似文献
15.
UML模型一致性自动检测的主要任务是解决形式化问题。描述逻辑是一阶谓词逻辑的可判定子集,具备强大的知识表示和推理功能。针对UML模型形式化问题,提出基于描述逻辑的形式化方法,分析UML类图各模型元素与描述逻辑SHOIN(D)的对应关系,提出UML类图的SHOIN(D)形式化方法,给出UML类图转换为SHOIN(D)知识库的正确性证明。 相似文献
16.
UML中的类图采用直观的图形化表示方法,有效描述了待建系统的静态特征,为系统设计人员发现系统模型中存在的不一致性和冗余等问题,提供了有效的分析工具。但是对于复杂的系统,完全依靠系统分析人员发现模型中存在的不一致性和冗余等问题是不现实的,应当为建模工具赋以模型自动一致性检查功能。SHOIQ(D)是描述逻辑家族中可判定的子集,它在保证推理可判定的同时,具备较强的描述知识能力。鉴于上述特点,通过从UML类图图元中抽取语义,用SHOIQ(D)形式化描述类图图元,借助自动推理引擎,从而使基于UML类图模型的自动一致性检查功能得到实现。根据该方法改进后的建模工具,可以自动发现基于UML类图模型中存在的不一致性和冗余等问题。 相似文献
17.
18.
为了扩展包括投资者建模、企业建模与扩展价值链建模的Martin/Odell OOA/D方法,该文章使用UML活动图扩展这些技术。UML提供了丰富的标记表示对分析系统行为和系统结构进行分析。其中活动图是用来描述系统的动态行为,并且也适用于业务过程建模。但由于UML的语义是用纯文本的方式描述的,通常不够准确,故而此文提出了使用ASM扩展语义的活动图描述包含上述建模技术的业务过程。 相似文献
19.
统一建模语言(UML)是一个半形式化的语言,其语义部分是采用自然语言描述的,使得它在建模过程中会产生语义不一致等问题。在详细比较UML类图与本体的基础上,提出了一种UML类图的形式化方法;首先将UML类图转换为相应的本体;然后根据本体提供的推理算法(Tableau)对转换得到的本体进行推理,检测其中的不一致性从而修改UML类图,最后达到精确UML类图。 相似文献