期刊文献+
共找到10篇文章
< 1 >
每页显示 20 50 100
UML 2.0顺序图的XYZ/E时序逻辑语义研究 被引量:11
1
作者 黄正宝 张广泉 《计算机科学》 CSCD 北大核心 2006年第8期249-251,共3页
UML2.0顺序图适合于描述软件体系结构的各个组件之间和复合组件内部各个子组件之间的动态交互行为,但由于UML2.0顺序图的语义不够精确,使得它的描述结果不利于进一步的分析和验证。基于此,本文在定义UML2.0顺序图的语法和语法约束的基础... UML2.0顺序图适合于描述软件体系结构的各个组件之间和复合组件内部各个子组件之间的动态交互行为,但由于UML2.0顺序图的语义不够精确,使得它的描述结果不利于进一步的分析和验证。基于此,本文在定义UML2.0顺序图的语法和语法约束的基础上,给出了UML2.0顺序图的XYZ/E时序逻辑语义,为使用UML2.0顺序图与XYZ/E相结合的方式来描述软件体系结构的动态交互行为奠定了基础。 展开更多
关键词 时序逻辑 形式化语义 uml2.0 顺序图 XYZ/E
下载PDF
UML 2.0的形式化语义研究 被引量:4
2
作者 张广泉 戎玫 黄正宝 《南京邮电大学学报(自然科学版)》 EI 2007年第3期39-43,共5页
由于UML2.0动态视图缺乏精确的语义,难以对它所表示的系统进行分析和验证。基于此,在描述UML2.0顺序图和状态图语法和语法约束的基础上,采用可执行的线性时序逻辑语言XYZ/E定义其形式化语义,这样不仅便于UML2.0顺序图和状态图之间的模... 由于UML2.0动态视图缺乏精确的语义,难以对它所表示的系统进行分析和验证。基于此,在描述UML2.0顺序图和状态图语法和语法约束的基础上,采用可执行的线性时序逻辑语言XYZ/E定义其形式化语义,这样不仅便于UML2.0顺序图和状态图之间的模型转换,也为使用UML和形式化方法相结合描述软件体系结构的交互行为奠定了基础。 展开更多
关键词 线性时序逻辑 形式化语义 uml2.0 顺序图 状态图 XYZ/E
下载PDF
基于事件确定有限自动机的UML2.0序列图描述与验证 被引量:8
3
作者 张琛 段振华 田聪 《软件学报》 EI CSCD 北大核心 2011年第11期2625-2638,共14页
为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata... 为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性. 展开更多
关键词 uml2.0序列图 事件确定有限自动机 模型检测 命题投影时序逻辑 验证
下载PDF
面向方面的软件系统动态交互行为建模 被引量:5
4
作者 杨敬中 戎玫 张广泉 《计算机工程与科学》 CSCD 2007年第11期137-139,共3页
面向方面编程是一种基于关注点分离的新技术,它成功地解决了面向对象编程中存在的代码缠结和散射问题。但是,在软件设计阶段,面向方面建模并没有得到很好的支持。通过分析面向方面编程的特点以及UML2.0新增的复合片段概念,本文提出了应... 面向方面编程是一种基于关注点分离的新技术,它成功地解决了面向对象编程中存在的代码缠结和散射问题。但是,在软件设计阶段,面向方面建模并没有得到很好的支持。通过分析面向方面编程的特点以及UML2.0新增的复合片段概念,本文提出了应用顺序图中的可选片段来表示Aspect与组件之间的横切交互行为,并给出将Aspect引入顺序图的相关规定,实现了UML2.0顺序图对面向方面建模的支持。 展开更多
关键词 面向方面建模 uml2.0顺序图 复合片段
下载PDF
UML2.0顺序图的时序描述逻辑语义 被引量:7
5
作者 张其文 童格明 李明 《计算机工程》 CAS CSCD 北大核心 2011年第3期52-54,共3页
针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新... 针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新增的交互操作符将UML2.0顺序图分成一个或多个最大顺序片段,通过形式化最大顺序片段和交互操作符得到UML2.0顺序图的时序描述逻辑语义。实例检验结果表明,该方法具有可行性。 展开更多
关键词 uml2.0顺序图 时序描述逻辑 形式化 描述逻辑
下载PDF
UML2.0顺序图的一种有穷自动机模型 被引量:3
6
作者 刘传会 戎玫 张广泉 《计算机工程与科学》 CSCD 2008年第12期118-121,141,共5页
为了在软件开发早期阶段对UML2.0顺序图模型进行分析和验证,本文给出了UML2.0顺序图的一种有穷自动机模型。首先给出了顺序图在语法和语义上的形式化描述,然后提出了一种使有穷自动机来描述每个对象在顺序图描述的场景中所参与的事件序... 为了在软件开发早期阶段对UML2.0顺序图模型进行分析和验证,本文给出了UML2.0顺序图的一种有穷自动机模型。首先给出了顺序图在语法和语义上的形式化描述,然后提出了一种使有穷自动机来描述每个对象在顺序图描述的场景中所参与的事件序列的方法,并将该方法扩展到带有组合片段的UML2.0顺序图,最后分析了UML2.0顺序图中的时间建模机制,设计了从UML2.0顺序图中提取时间约束的算法。以上工作为使用模型检测工具UPPAAL对顺序图模型进行进一步的分析与验证奠定了基础。 展开更多
关键词 uml2.0顺序图 UPPAAL 有穷自动机 时间自动机
下载PDF
基于通信序列进程的UML序列图形式化方法 被引量:1
7
作者 邓建波 张立臣 +1 位作者 邓惠敏 徐碧红 《计算机应用》 CSCD 北大核心 2010年第10期2727-2729,2734,共4页
UML2.0序列图是一种描述对象之间动态协作和事件发展时间关系的视图,但是UML序列图缺乏精确的形式化语义,所以不利于对其所描述的系统进行形式化验证。为此,根据UML2.0语义文档及组合碎片包概念,基于通信序列进程(CSP)给出了UML序列图... UML2.0序列图是一种描述对象之间动态协作和事件发展时间关系的视图,但是UML序列图缺乏精确的形式化语义,所以不利于对其所描述的系统进行形式化验证。为此,根据UML2.0语义文档及组合碎片包概念,基于通信序列进程(CSP)给出了UML序列图的基本元素和消息迹的形式化定义及生成规则,实现了UML序列图的形式化,为UML序列图在描述系统准确性和有效性方面提供了形式化的检验方法。最后通过ATM实例说明UML序列图这一过程的正确性。 展开更多
关键词 uml2.0序列图 形式语义 组合碎片包 通信序列进程
下载PDF
基于UML2.0的软件安全测试方法 被引量:1
8
作者 张琛 段振华 《武汉大学学报(理学版)》 CAS CSCD 北大核心 2010年第2期165-169,共5页
提出了一种从UML2.0序列图产生软件安全测试用例的方法,该方法以基于模型的测试技术为基础,将序列图转换为事件迁移图,从而产生测试用例集,提高了软件安全性测试的自动化水平.该方法可应用于软件设计与开发过程的早期阶段.所添加的UML2.... 提出了一种从UML2.0序列图产生软件安全测试用例的方法,该方法以基于模型的测试技术为基础,将序列图转换为事件迁移图,从而产生测试用例集,提高了软件安全性测试的自动化水平.该方法可应用于软件设计与开发过程的早期阶段.所添加的UML2.0序列图的新特征,可将传统的软件测试方法应用于软件安全性测试. 展开更多
关键词 软件安全测试 uml2.0序列图 测试用例 事件迁移图
原文传递
基于消息语义的UML2.0顺序图控制流分析
9
作者 王洪媛 王琳 +1 位作者 张家晨 金淳兆 《吉林大学学报(理学版)》 CAS CSCD 北大核心 2007年第4期595-600,共6页
基于消息语义提出一种分析UML2.0顺序图控制流的方法,分析了UML2.0顺序图消息发送和接收动作之间的关系,并将其映射到相应的消息上,得到消息的相继顺序关系.根据消息的顺序关系设计了由顺序图到活动图的一致性映射规则,并得到基于消息... 基于消息语义提出一种分析UML2.0顺序图控制流的方法,分析了UML2.0顺序图消息发送和接收动作之间的关系,并将其映射到相应的消息上,得到消息的相继顺序关系.根据消息的顺序关系设计了由顺序图到活动图的一致性映射规则,并得到基于消息语义的并发控制流图(MSCCFG),从而获取顺序图的控制流信息. 展开更多
关键词 uml2.0顺序图 活动图 控制流分析 并发控制流 消息 动作
下载PDF
一种UML2.0模型动态特性的一致性验证方法
10
作者 雷博 裴磐洁 《信息技术》 2014年第8期183-186,共4页
近年来,UML已经被广泛应用于软件的分析和设计,然而,由于软件系统的复杂性,在UML模型中,难免会引入不同图表间特别是动态视图之间的不一致性。提出了一种用于验证UML2.0模型状态图和顺序图一致性的方法。首先,用XYZ/E来形式化描述状态... 近年来,UML已经被广泛应用于软件的分析和设计,然而,由于软件系统的复杂性,在UML模型中,难免会引入不同图表间特别是动态视图之间的不一致性。提出了一种用于验证UML2.0模型状态图和顺序图一致性的方法。首先,用XYZ/E来形式化描述状态图并将其转化为Promela输入语言;然后,用LTL来表示顺序图间的相互作用;最后利用模型检测工具Spin通过检查Promela描述的状态图是否满足LTL公式来达到检测模型一致性的目的。 展开更多
关键词 uml2 0 状态图 顺序图 一致性 模型检测
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部