2. 您的位置
3. 首页
4. 期刊论文
5. 基于时间自动机的UML模型转换与验证研究

基于时间自动机的UML模型转换与验证研究

来源 :郑州大学学报：理学版 | 被引量 : 0次 | 上传用户：eagleqizha

【摘 要】

：

针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转

【作 者】

：

姬莉霞 马建红 

【机 构】

：

郑州大学软件技术学院

【出 处】

：

郑州大学学报：理学版

【发表日期】

：

2013年1期

【关键词】

：

统一建模语言 模型验证 模型转换 UPPAAL 时间自动机 元模型 UML model checking model transformation Uppaal 

【基金项目】

：

河南省科技攻关计划项目,编号122102210518,河南省教育厅科学技术研究项目,编号12A520042

下载到本地 , 更方便阅读

下载此文 赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.

其他文献

基于DSP控制的单相光伏并网逆变系统设计

基于TMS320F2812芯片,阐述了一种单相光伏并网逆变系统的设计与实现方法.分析并设计了系统主电路,介绍了最大功率跟踪算法、电网跟踪控制以及电网电压锁相环的设计方法,并使

期刊

光伏逆变系统MPPT锁相photovoltaic inverter system MPPT phase locking

基于效用最大化理论关于保险人监管成本的分析

运用期望效用最大化理论建立数学模型，主要分析保险人在偿付能力不足的条件下选择是否进行再保险时对投保人的最优监管水平．同时结合实际，提出一些关于加强保险人道德水平的建议

期刊

效用最大化保险人偿付能力再保险监管水平maximization of utility insurers solvency reinsura

H-矩阵的预条件AOR迭代法

H-矩阵是一类用途比较广泛的矩阵,为了解决H-矩阵线性系统,给出了两类新的不同预条件AOR迭代法,得到了这两类预条件AOR迭代法的收敛结果.最后用数值例子验证得到的结果是正确

期刊

H-矩阵M-矩阵AOR迭代法谱半径收敛性H-matrix M-matrix AOR iterative method spectral radi

四阶混合边值问题的广义Jacobi-Petrov-Galerkin谱方法

发展了矩形区域上的四阶混合边值问题的广义Jacobi—Petrov-Galerkin谱方法，利用广义Jacobi多项式对模型问题的精确解进行数值展开，设计了有效的数值算法．数值结果验证了该算法

期刊

四阶混合边值问题广义Jacobi—Petrov—Galerkin谱方法广义Jacobi—Gauss—Lobatto插值fourth-order mixed

滤正则序列与局部上同调

对交换代数中正则序列和深度的概念进行了推广,并利用局部上同调、短正合列诱导长正合列等同调代数手段及伴随素理想、局部化等交换代数内容和方法对推广的深度给了一些刻画.

期刊

滤正则序列深度局部上同调支集filter regular sequence depth local cohomology support

N-（1-（5-溴-2-（（4-氯苄基）氧基）苄基）哌啶-4-基）-3-氯-N-乙基苯甲酰胺的合成及表征

CCR5作为一种可利用的新靶点,用以防治人类HIV感染.以5-溴水杨醛、4-氯苄氯为原料,通过消去、还原及溴化合成了4-溴-2-溴甲基-1-（（4-氯苄基）氧）苯（Ⅲ）,以哌啶-4-酮为原料合成了3-氯

期刊

拮抗剂非肽类小分子化合物合成表征antagonist non-peptide small molecular compound synthesis

Banach空间分数阶微分方程边值问题解的存在性

考虑Banach空间E中分数阶微分方程边值问题{-Dβ0＋u（t）=f（t,u（t））,t∈Ju（0）=u（1）={θ解的存在性,其中1〈β≤2为实数,J=[0,1],Dβ0＋是标准的Riemann-Liouville导数,f：J×E→E连续.用新

期刊

分数阶微分方程凝聚映射不动点定理非紧性测度边值问题fractional differential equation condensing mappi

基于单元概率重要度的黄标车限行策略研究

基于城市道路网络系统可靠度理论,对郑州市区三环内的道路网络进行了基于蒙特卡罗的模拟分析.通过单元概率重要度的计算,确定重要度较大的路段集和区域,结合实践调查数据,提

期刊

道路交通黄标车限行策略单元概率重要度road traffic yellow-label vehicle restriction strategy

一类非线性四阶差分方程边值问题正解的存在性准则

运用不动点指数理论，获得了非线性四阶差分方程边值问题 正解的存在性准则，其中，T2={2，3，…，r，}，f：T2×R→[0，∞）连续且T〉4，A〉0为参数．

期刊

四阶差分方程正解存在性不动点指数fourth-order difference equation positive solution existen

内蒙古草乌中氨基酸提取工艺的研究及测定

以盐酸为提取溶剂,通过加热回流对草乌中氨基酸进行提取,确定了氨基酸提取的最佳工艺条件,并使用氨基酸自动分析仪测定其组成含量.结果表明：最佳提取条件为料液比1∶50,提取时

期刊

草乌氨基酸提取分析Radix Aconiti Kusenezoffii amino acid extraction analysis