期刊文献+
共找到30篇文章
< 1 2 >
每页显示 20 50 100
基于模型的IMA时间资源配置验证方法研究 被引量:6
1
作者 王明明 胡军 +1 位作者 张维珺 李宛倩 《计算机技术与发展》 2018年第5期32-37,共6页
综合模块化航空电子系统(IMA)在飞机机载航空电子系统领域应用广泛,已经成为飞机机载系统的重要的系统结构和发展趋势。IMA具有高安全性,资源共享和高度模块化综合化的特征,模块或组件间以AFDX网络连接。在IMA系统开发的过程中,为确保... 综合模块化航空电子系统(IMA)在飞机机载航空电子系统领域应用广泛,已经成为飞机机载系统的重要的系统结构和发展趋势。IMA具有高安全性,资源共享和高度模块化综合化的特征,模块或组件间以AFDX网络连接。在IMA系统开发的过程中,为确保系统的可靠性和安全性,IMA资源配置必须是正确的和安全有效的。所以对IMA进行有效的系统资源配置并保证配置的正确性和安全性成为航电领域一项重要的研究内容。结合IMA系统的特征,提出了一种基于模型的IMA系统时间资源配置的验证方法。建立IMA系统时间行为的MARTE模型,使用可调度分析工具MAST,分析系统时间资源的可调度性,仿真分析、验证IMA配置与需求之间的满足性。并结合IMA系统中的一个水处理系统的实例来进行分析验证。 展开更多
关键词 综合航电系统 模型驱动工程 marte 系统资源配置 MAST
下载PDF
基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究 被引量:5
2
作者 黄传林 黄志球 +2 位作者 胡军 徐丙凤 曲长亮 《小型微型计算机系统》 CSCD 北大核心 2015年第3期408-417,共10页
能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型... 能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究;包括:构建了Sys ML活动图与MARTE中非功能性质建模语义相结合的元模型,以及验证工具UPPAAL的时间自动机元模型,并且给出了二者之间的语义映射规则;建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法;设计了一个基于AMMA平台的面向扩展Sys ML活动图的模型转换与验证框架;最后,给出了一个高铁控制系统设计模型的安全性验证的实例分析. 展开更多
关键词 嵌入式系统安全性分析 SysML活动图 marte 模型转换 形式化方法
下载PDF
模型驱动的安全关键系统重配置信息验证方法 被引量:4
3
作者 胡军 马金晶 +3 位作者 刘雪 程桢 石娇洁 黄志球 《计算机科学与探索》 CSCD 北大核心 2015年第4期385-402,共18页
近年来,在以综合模块化航电系统(integrated modular avionics,IMA)为代表的一类安全关键应用中,确保系统重配置信息的正确性成为保证系统安全可靠运行的一个重要问题。提出了一种模型驱动架构下符合ARINC653规范的IMA系统配置信息的建... 近年来,在以综合模块化航电系统(integrated modular avionics,IMA)为代表的一类安全关键应用中,确保系统重配置信息的正确性成为保证系统安全可靠运行的一个重要问题。提出了一种模型驱动架构下符合ARINC653规范的IMA系统配置信息的建模转换与验证方法。针对多个实时应用在IMA平台上以时间/空间多分区形式运行的系统特征,建立了从系统配置信息的核心元素(包括模块、分区、内存、进程、通信等)到MARTE模型元素的语义映射规则,设计了基于模型驱动架构的系统配置信息模型转换的方法,并给出了一种对模型转换构造得到的系统配置信息MARTE模型进行形式化验证的框架。最后,通过一个实例分析说明了此方法对验证重配置后系统配置信息的有效性。 展开更多
关键词 系统配置信息验证 marte 模型驱动工程 ARINC653 综合模块化航电系统(IMA)
下载PDF
基于MDA的实时软件资源建模与模型转换的方法 被引量:4
4
作者 吉鸣 黄志球 +2 位作者 祝义 王珊珊 沈国华 《计算机科学》 CSCD 北大核心 2011年第8期136-141,共6页
模型驱动体系结构(MDA)是一种以模型为中心的软件开发框架,其本质是元建模与模型转换。提出了一种基于MDA的实时软件资源建模与模型转换的方法。首先通过元建模抽象出包含资源信息的MARTE元模型以及价格时间自动机的元模型;然后利用模... 模型驱动体系结构(MDA)是一种以模型为中心的软件开发框架,其本质是元建模与模型转换。提出了一种基于MDA的实时软件资源建模与模型转换的方法。首先通过元建模抽象出包含资源信息的MARTE元模型以及价格时间自动机的元模型;然后利用模型转换语言ATL对MARTE元模型和价格时间自动机元模型构造转换规则,通过将对应的实例模型进行相互转换,实现在MDA下MARTE模型到价格时间自动机模型的转换;最后通过形式化工具UPPAAL对模型转换结果进行形式化验证。实例分析表明了该方法的可行性与有效性,它能够提高实时软件资源建模的可信性。 展开更多
关键词 模型驱动体系结构 元建模 marte 模型转换 价格时间自动机
下载PDF
带数据约束实时系统的模型检测 被引量:4
5
作者 倪水妹 曹子宁 李心磊 《计算机科学》 CSCD 北大核心 2014年第5期254-262,269,共10页
带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个模型中的规范及验证研究较少。文中提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的... 带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个模型中的规范及验证研究较少。文中提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的ZIA规范,并给出它的时序逻辑。MARTE是UML在嵌入式实时系统领域的建模规范,在工业界的应用非常广泛,但是目前对其模型检测的研究较少。在MARTE的基础上扩展Z,提出了Z-MARTE,并将Z-MARTE转换为基于连续时间的ZIA模型,在实现对连续时间ZIA模型检测的同时,也实现了对Z-MARTE的模型检测。最后通过一个实例进行验证,说明此方法可行有效。 展开更多
关键词 数据约束 实时系统 连续时间 marte ZIA 模型检测
下载PDF
Hybrid MARTE statecharts 被引量:2
6
作者 Jing LIU Ziwei LIU +2 位作者 Jifeng HE Freederic MALLET Zuohua DING 《Frontiers of Computer Science》 SCIE EI CSCD 2013年第1期95-108,共14页
The specification of modeling and analysis of real-time and embedded systems (MARTE) is an extension of the unified modeling language (UML) in the domain of real-time and embedded systems. Even though MARTE time m... The specification of modeling and analysis of real-time and embedded systems (MARTE) is an extension of the unified modeling language (UML) in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specifi- cation and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to ex- tend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that: the logical time variables and the chronometric time vari- ables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition sys- tems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit. 展开更多
关键词 UML marte hybrid automata hybrid marte statechart train control system
原文传递
基于模型驱动的嵌入式软件测试技术研究 被引量:2
7
作者 雷海申 王轶辰 《网络空间安全》 2016年第8期75-83,共9页
软件测试是保证软件可靠性的一种最重要的手段,而软件自动化测试又是保证软件测试效率的一种十分有效的方式。基于模型驱动的软件测试是一种自动化程度较高的测试方法。论文对模型驱动测试技术进行了综述,对测试需求建模、PIM转换到测... 软件测试是保证软件可靠性的一种最重要的手段,而软件自动化测试又是保证软件测试效率的一种十分有效的方式。基于模型驱动的软件测试是一种自动化程度较高的测试方法。论文对模型驱动测试技术进行了综述,对测试需求建模、PIM转换到测试模型、测试用例生成方法的相关文献进行了调研。 展开更多
关键词 模型驱动测试 测试需求建模 UML marte
下载PDF
UML活动图到时间Petri网的映射方法 被引量:1
8
作者 顾炜 黄志球 李剑 《电子科技》 2012年第2期105-108,共4页
UML被广泛应用于嵌入式实时系统等领域的建模,而嵌入式实时系统对时间响应的要求非常严格,UML缺乏对系统时间约束的描述和形式化语义。因此,提出了一种结合MARTE与UML带有时间约束的UML活动图模型,并定义相应的映射规则,将该活动图模型... UML被广泛应用于嵌入式实时系统等领域的建模,而嵌入式实时系统对时间响应的要求非常严格,UML缺乏对系统时间约束的描述和形式化语义。因此,提出了一种结合MARTE与UML带有时间约束的UML活动图模型,并定义相应的映射规则,将该活动图模型映射到时间Petri网模型,最后通过实例验证了该映射方法的正确性和实用性。 展开更多
关键词 UML活动图 marte 时间PETRI网
下载PDF
从UML到GSPN的转换和性能分析方法 被引量:1
9
作者 胡翔 焦莉 柴叶生 《计算机科学》 CSCD 北大核心 2016年第11期49-54,共6页
UML模型一般不能直接进行性能分析,需要利用模型转换的方法将其转换成其他分析模型,比如排队论、随机进程代数或者随机Petri网等模型。利用Eclipse平台上的Papyrus建立3种类型的UML模型(用例图、部署图和活动图)来对系统进行建模,并利用... UML模型一般不能直接进行性能分析,需要利用模型转换的方法将其转换成其他分析模型,比如排队论、随机进程代数或者随机Petri网等模型。利用Eclipse平台上的Papyrus建立3种类型的UML模型(用例图、部署图和活动图)来对系统进行建模,并利用MARTE规范添加一些性能相关的信息;然后利用ATL实现UML模型到广义随机Petri网(GSPN)模型的转换,并使用XStream将上一步得到的GSPN模型转换成分析工具所支持的格式;最后利用基于GSPN的性能分析方法进行系统性能分析。同时给出了一系列性能指标的计算方法,如利用率、吞吐量、平均等待请求的数目以及响应时间等,可以考察系统性能的多个方面,方便系统设计和开发人员对系统性能进行分析和优化。 展开更多
关键词 模型驱动工程 UML PETRI网 模型转换 marte
下载PDF
基于模型转换的MARTE顺序图的形式化分析 被引量:1
10
作者 朱梅霞 王捍贫 +1 位作者 刘西奎 韩晓琼 《小型微型计算机系统》 CSCD 北大核心 2013年第1期100-106,共7页
作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行... 作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TTS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD,用TTS4SD描述顺序图的形式语义,最后对TTS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法. 展开更多
关键词 实时系统 形式化方法 marte 时间变迁系统 验证
下载PDF
时序π演算及其对MARTE顺序图的建模
11
作者 金暐 王捍贫 +1 位作者 曹永知 朱梅霞 《武汉大学学报(理学版)》 CAS CSCD 北大核心 2011年第6期506-510,共5页
MARTE是统一建模语言UML在实时和嵌入式方面的一个扩展.本文给出π演算的一个带时序的变体来对MARTE顺序图的主要元素进行建模.相对于传统的π演算来说,时序π演算中增加了时间算子,可以对时间的流逝和计时器事件进行描述.同时,给出了... MARTE是统一建模语言UML在实时和嵌入式方面的一个扩展.本文给出π演算的一个带时序的变体来对MARTE顺序图的主要元素进行建模.相对于传统的π演算来说,时序π演算中增加了时间算子,可以对时间的流逝和计时器事件进行描述.同时,给出了时序π演算的语法和语义,并定义了时序π进程间的强互模拟关系.基于时序π演算,定义了MARTE顺序图的形式化模型,从而给出了MARTE顺序图的完整语义,并为进一步的模型检测提供了理论基础. 展开更多
关键词 时序π演算 marte 顺序图
原文传递
Scenario-based verification in presence of variability using a synchronous approach
12
作者 Jean-Vivien MILLO Frederic MALLET +1 位作者 Anthony COADOU S RAMESH 《Frontiers of Computer Science》 SCIE EI CSCD 2013年第5期650-672,共23页
This paper presents a new model of scenarios, dedicated to the specification and verification of system be- haviours in the context of software product lines (SPL). We draw our inspiration from some techniques that ... This paper presents a new model of scenarios, dedicated to the specification and verification of system be- haviours in the context of software product lines (SPL). We draw our inspiration from some techniques that are mostly used in the hardware community, and we show how they could be applied to the verification of software components. We point out the benefits of synchronous languages and mod- els to bridge the gap between both worlds. 展开更多
关键词 ESTEREL UML marte SCENARIO verification feature interaction VARIABILITY
原文传递
基于UML MARTE处理AADL的端到端流延迟
13
作者 杨夏 《软件工程师》 2015年第11期24-26,共3页
AADL和MARTE都支持对实时嵌入式系统形式化建模的分析。利用MARTE的时间模型设备,研究MARTE是如何对实时嵌入式系统的建模和分析的,能够比较准确的通过事件或者数据端口的端到端流延迟分析,表达AADL周期性或非周期性任务。
关键词 AADL marte 流延迟
下载PDF
基于MARTE的IMA系统时间资源可调度配置验证
14
作者 程桢 《电子世界》 2016年第4期183-184,共2页
目前综合模块化航空电子系统(IMA)在资源配置方面有非常高的安全可靠性需求,其中时间资源的可调度性配置验证也显得至关重要。本文在AFDX网络架构下提出了一种IMA系统时间相关概念的MARTE建模和时间资源可调度配置的正确性验证方法。建... 目前综合模块化航空电子系统(IMA)在资源配置方面有非常高的安全可靠性需求,其中时间资源的可调度性配置验证也显得至关重要。本文在AFDX网络架构下提出了一种IMA系统时间相关概念的MARTE建模和时间资源可调度配置的正确性验证方法。建立了IMA系统通信虚拟链路、AFDX终端、分区以及进程等相关元素到MARTE模型元素的建模规则,并设计了基于可调度分析工具MAST的时间资源可调度配置验证框架,最后利用相关实例进行仿真和分析得到验证结果。 展开更多
关键词 综合航电系统 模型驱动工程 marte 系统资源配置
下载PDF
基于MDE的异构模型转换:从MARTE模型到FIACRE模型 被引量:9
15
作者 张天 Frédéric JOUAULT +2 位作者 Christian ATTIOGBE Jean BEZIVIN 李宣东 《软件学报》 EI CSCD 北大核心 2009年第2期214-233,共20页
通过研究一个具有代表性的UML/MARTE(unified modeling language/modeling and analysis of real time and embedded systems)模型向FIACRE(intermediate format for the architectures of embedded distributed components)形式模型的... 通过研究一个具有代表性的UML/MARTE(unified modeling language/modeling and analysis of real time and embedded systems)模型向FIACRE(intermediate format for the architectures of embedded distributed components)形式模型的转换实例,探讨了异构模型之间在语义和语法层的相互转换问题.在语义层,通过模型转换技术构造语义映射规则,实现元语言之间的转换;在语法层,通过构造元模型的具体语法,反映元语言的语法规则,从而产生目标模型的程序实体.基于此实例研究,探讨了通用转换途径的相关框架和关键技术,并讨论了转换工作的优缺点和实用性. 展开更多
关键词 模型驱动工程 形式化方法 marte(modeling and analysis of real time and embedded systems) FIACRE (intermediate format for the architectures ofembedded distributed components) 异构性
下载PDF
基于元建模的实时系统模型转换方法研究 被引量:8
16
作者 刘亚萍 黄志球 祝义 《小型微型计算机系统》 CSCD 北大核心 2010年第11期2145-2153,共9页
通过模型转换将UML模型转换为形式化模型并进行模型检验是软件工程研究领域的热点,然而传统的模型转换多是ad-hoc式的,转换规则复杂且难以重用.本文针对这一研究现状,通过元建模实现MARTE到时间自动机模型的转换,从而提出一种基于元建... 通过模型转换将UML模型转换为形式化模型并进行模型检验是软件工程研究领域的热点,然而传统的模型转换多是ad-hoc式的,转换规则复杂且难以重用.本文针对这一研究现状,通过元建模实现MARTE到时间自动机模型的转换,从而提出一种基于元建模的实时系统模型转换方法.该方法有效的分离了语法转换与语义转换,框架标准的支撑使得转换易于重用.最后通过一个实例来说明该方法的可行性与有效性. 展开更多
关键词 模型转换 marte(modeling and analysis of REAL TIME and embeded systems) 模型验证 时间自动机
下载PDF
基于MDA的MARTE模型形式化方法 被引量:4
17
作者 许海洋 王萍 《计算机应用研究》 CSCD 北大核心 2012年第8期3018-3021,共4页
针对嵌入式系统对可靠性和可预测性的要求,提出基于MDA对嵌入式系统的建模语言MARTE进行形式化描述的方法。建立Object-Z的元模型,定义了MARTE元模型与Object-Z元模型之间的模型转换关系,给出了MARTE模型到Object-Z模型的语义映射和语... 针对嵌入式系统对可靠性和可预测性的要求,提出基于MDA对嵌入式系统的建模语言MARTE进行形式化描述的方法。建立Object-Z的元模型,定义了MARTE元模型与Object-Z元模型之间的模型转换关系,给出了MARTE模型到Object-Z模型的语义映射和语法转换的具体过程。该方法支持将MARTE模型形式化转换为Object-Z模型,有利于软件开发早期的检验和验证。 展开更多
关键词 模型驱动体系 形式化方法 模型转换 marte元模型
下载PDF
基于DFT-MARTE模型的时序分析算法
18
作者 徐嘉 周晴 +1 位作者 杜家昊 王一华 《计算机工程与设计》 北大核心 2024年第1期120-129,共10页
针对航天嵌入式软件(aerospace embedded software,AES)时序需求复杂带来的时序需求定义不准确问题,提出一种基于MARTE(modeling and analysis of real-time and embedded systems)模型的数据流时序(data flow timing based on MARTE,DF... 针对航天嵌入式软件(aerospace embedded software,AES)时序需求复杂带来的时序需求定义不准确问题,提出一种基于MARTE(modeling and analysis of real-time and embedded systems)模型的数据流时序(data flow timing based on MARTE,DFT-MARTE)模型,设计基于该模型的处理点缓存计算算法、时序偏离概率检测算法和时序序列分析算法。处理点缓存计算算法动态更新缓存空间,使后续时序检测正常执行;时序偏离概率检测算法利用多线程并发模拟时序特性,检测需求中时序偏离问题;时序序列分析算法是基于梯度下降算法,拟合时序序列,指导用户优化需求。该模型相比传统数据流模型更适用航天嵌入式软件,利于后续开发和维护,具有极高的应用价值。 展开更多
关键词 数据流时序模型 数据流图 嵌入式软件 时序偏离检测 多线程 时序分析 梯度下降算法
下载PDF
一种基于SysML/MARTE/pCCSL的信息物理融合系统协同建模方法 被引量:3
19
作者 黄平 杜德慧 《华东师范大学学报(自然科学版)》 CAS CSCD 北大核心 2019年第1期48-57,共10页
信息物理融合系统(Cyber-Physical Systems, CPS)是一个综合计算、网络和物理环境的多维复杂系统.针对这种异构系统的建模问题一直是人们研究的重点,但是,缺乏系统性的方法来建模CPS的特性,如异构性、不确定性、软硬协同和非功能属性(No... 信息物理融合系统(Cyber-Physical Systems, CPS)是一个综合计算、网络和物理环境的多维复杂系统.针对这种异构系统的建模问题一直是人们研究的重点,但是,缺乏系统性的方法来建模CPS的特性,如异构性、不确定性、软硬协同和非功能属性(Non-Functional Properties, NFP)等.提出了一种基于SysML (System Modeling Language)/MARTE (Modeling and Analysis of Real-Time and Embedded Systems)/pCCSL (p Clock Constraint Specification Language)的协同建模方法,实现了从不同视角建模CPS的不同特征,包括系统的结构、行为、时钟约束和NFP.该方法的新颖性在于使用pCCSL规约各模型之间的交互和同步,显式地建模模型之间的逻辑一致性.同时,为了捕捉CPS的特性如随机行为和连续行为,扩展了一些SysML/MARTE的元模型.最后,给出了一个智能建筑的案例以展示所提出的协同建模方法的可用性. 展开更多
关键词 信息物理融合系统 SysML/marte/pCCSL 协同建模 元模型 智能建筑
下载PDF
基于MDA的MARTE模型形式化转换 被引量:2
20
作者 王立杰 刘昌禄 俞烈彬 《指挥控制与仿真》 2012年第6期128-133,共6页
非形式化/半形式化模型到形式化模型之间的转换是当前软件工程领域的研究热点。根据异构模型转换,提出了基于MDA的MARTE模型到Object-Z规约之间的转换方法。针对Object-Z在实时领域表达能力不足的问题,首先扩展Object-Z元模型;然后在MD... 非形式化/半形式化模型到形式化模型之间的转换是当前软件工程领域的研究热点。根据异构模型转换,提出了基于MDA的MARTE模型到Object-Z规约之间的转换方法。针对Object-Z在实时领域表达能力不足的问题,首先扩展Object-Z元模型;然后在MDA的元元模型体系下,定义了MARTE元模型和扩展的Object-Z元模型之间的转换规则。MARTE模型可以重用这些转换规则以实现到Object-Z形式化描述之间的转换,进而可以对模型进行形式化验证;最后通过一个实例使用该方法完成模型转换,具体说明了转换规则的应用。 展开更多
关键词 模型驱动 marte模型 Object-Z规约 元模型 模型转换
下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部