检索结果-南通市图书馆

基于模型转换的marte顺序图的形式化分析

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

小型微型计算机系统 2013年第1期34卷 100-106页

作者：朱梅霞王捍贫刘西奎韩晓琼天津工业大学计算机科学与软件学院天津300387 北京大学信息科学技术学院软件研究所北京100871 教育部高可信软件技术重点实验室北京100871 山东科技大学信息科学与工程学院山东青岛266510

作为一项新规范,marte有许多方面亟待完善.如何对依照marte设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照marte设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行... 详细信息

作为一项新规范,marte有许多方面亟待完善.如何对依照marte设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照marte设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TTS4SD,用来描述marte规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD,用TTS4SD描述顺序图的形式语义,最后对TTS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法.

关键词：实时系统形式化方法 marte 时间变迁系统验证

在线全文

学校读者我要写书评

暂无评论

时序π演算及其对marte顺序图的建模

武汉大学学报（理学版） 2011年第6期57卷 506-510页

作者：金暐王捍贫曹永知朱梅霞北京大学信息科学技术学院北京100871

marte是统一建模语言UML在实时和嵌入式方面的一个扩展.本文给出π演算的一个带时序的变体来对marte顺序图的主要元素进行建模.相对于传统的π演算来说,时序π演算中增加了时间算子,可以对时间的流逝和计时器事件进行描述.同时,给出了... 详细信息

marte是统一建模语言UML在实时和嵌入式方面的一个扩展.本文给出π演算的一个带时序的变体来对marte顺序图的主要元素进行建模.相对于传统的π演算来说,时序π演算中增加了时间算子,可以对时间的流逝和计时器事件进行描述.同时,给出了时序π演算的语法和语义,并定义了时序π进程间的强互模拟关系.基于时序π演算,定义了marte顺序图的形式化模型,从而给出了marte顺序图的完整语义,并为进一步的模型检测提供了理论基础.

关键词：时序π演算 marte 顺序图

基于marte的综合航电系统配置信息分析与验证方法研究

在线全文

学校读者我要写书评

暂无评论

基于MARTE的综合航电系统配置信息分析与验证方法研究

作者：马金晶南京航空航天大学

学位级别：硕士

近年来综合模块化航电系统(IMA)已经成为航空应用领域中出现的一类重要系统结构和发展趋势;其中一类IMA架构标准就是ARINC653标准,定义了IMA平台中操作系统层和应用软件层之间的标准接口(APEX)。满足ARINC653标准的IMA系统称之为ARINC65... 详细信息

近年来综合模块化航电系统(IMA)已经成为航空应用领域中出现的一类重要系统结构和发展趋势;其中一类IMA架构标准就是ARINC653标准,定义了IMA平台中操作系统层和应用软件层之间的标准接口(APEX)。满足ARINC653标准的IMA系统称之为ARINC653系统。在IMA架构中,系统的配置信息(Configuration)包含了整个体系结构中所有层次的相关信息,用来对IMA系统的硬件接口、操作系统和应用程序进行详尽的参数配置。因此,系统配置信息决定了ARINC653系统能否正确可靠的运行,如何保证配置信息的正确性和完整性已经成为当前综合航电系统研究领域的一个重要问题。本文工作主要以嵌入式系统建模与分析规范(marte)结合形式化验证方法来对ARINC653系统的配置信息的正确性以及相关分区任务可调度性问题展开研究,具体研究内容如下所述:1)针对符合ARINC653标准的IMA系统,结合多个实时应用在IMA平台上以时间/空间多分区形式运行的系统特征,建立了从系统配置信息的核心元素(包括模块、分区、内存、进程、通信等)到marte模型元素的语义映射规则,设计了基于模型驱动架构的系统配置信息模型转换的方法。2)针对ARINC653系统配置正确性验证需求,给出了一种对模型转换构造得到的系统配置信息marte模型进行形式化验证的框架;根据核心配置信息的语义验证需求,设计相应的REAL定理;基于REAL定理,对生成的模型文件进行需求约束的形式化验证;通过模型验证方法找出配置信息中的错误,使得可以及时调整相应模块的配置,提高系统的安全性和可靠性。3)研究了在ARINC653系统中多任务实时调度可满足性的问题,首先,考虑ARINC653分区系统的运行特征,采用marte建模语言对ARINC653系统的分层调度策略进行建模,然后通过MAST工具自定义调度策略,设计了对包含分区任务集调度信息的marte模型进行可调度性判定的算法。4)基于Papyrus建模平台,设计并实现了一个用于ARINC653配置文件建模与验证的原型工具CC653(Configuration Checker for ARINC653)。通过对CC653工具进行了相关实例分析,说明了此方法可以验证IMA系统配置信息的正确性、分区任务可调度性。

关键词：综合航电系统 ARINC653配置信息 marte Papyrus MAST 可调度性判定

基于marte的时序需求建模与分析验证技术研究

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于MARTE的时序需求建模与分析验证技术研究

作者：徐嘉中国科学院大学(中国科学院国家空间科学中心)

学位级别：硕士

随着航天事业的迅速发展,嵌入式软件在航天整体系统设计、实现中的比重不断提高,繁重的任务需求进一步提升了航天嵌入式软件的规模及复杂度。时序是嵌入式软件的关键特性,时序正确决定了软件系统的稳定性。为了解决当前航天嵌入式软件... 详细信息

随着航天事业的迅速发展,嵌入式软件在航天整体系统设计、实现中的比重不断提高,繁重的任务需求进一步提升了航天嵌入式软件的规模及复杂度。时序是嵌入式软件的关键特性,时序正确决定了软件系统的稳定性。为了解决当前航天嵌入式软件时序需求复杂带来的时序需求定义不准确和需求分解不完整等问题,本文提出了一种基于marte模型的数据流时序模型,并在该模型的基础上设计了一种时序偏离检测分析算法和需求完整性验证算法,实现了一套时序需求分析验证系统,可以为软件设计师在需求分析阶段尽早开展软件时序分析验证工作。本文的具体工作如下:(1)由于航天嵌入式软件需求中包含了复杂的时序数据交互关系,传统的需求模型无法针对具有时序特性的数据流进行建模,因此,本文将传统数据流图和marte中的时序特性相融合,提出了一种基于marte模型的数据流时序模型。本模型将marte中时序模式融合入DFD的组件中,并在模型中增添数据优先级和事件触发的相关设计,重新构建元模型,使其满足航天嵌入式软件建模需求。(2)针对航天嵌入式软件需求时序需求复杂,需求人员很难发现定义的时序特性存在偏差的情况,本文提出了一种时序偏离检测分析算法,包含可达性分析、时序偏离概率计算、时序序列分析三个部分。软件系统中并不是所有的外部输入数据流通过系统后均可到达外部接口,为了进行后续时序偏离检测分析,首先需要进行可达性分析,找出所有可达外部输出且连接着数据汇点的数据流集合;时序偏离概率计算是依据软件需求通过模拟输入流的时序特性,计算匹配后输出流的时序特性,并将验证结果与期望时序特性进行比对,获得输出数据流的时序偏离概率。在上述的仿真模拟过程中,为了满足航天嵌入式软件中存在具有优先级数据的需求,在处理点模块中通过增添了优先队列和普通队列,来划分到达处理点的优先级和非优先级数据,并通过排队队列缓存输出流数据到达的时序信息,有利于后续的时序分析。时序序列分析采用基于梯度下降算法对上述得到的数据到达时序信息进行拟合,最终给出推荐的输出数据的时序特性,给需求分析人员作为时序改进的参考建议。(3)为了解决复杂需求在分解过程中易出现层级间信息不一致的问题,本文提出一种需求完整性验证算法。传统的模型一致性检查算法是针对数据流进行平衡性的检查,本算法在此基础上增添了节点的平衡性和正确性检查以及数据流的正确性检查,验证算法更全面。(4)设计并实现了面向航天嵌入式软件时序需求分析验证工具,实现以上算法,最终可以以XML文件形式导出含时间特性的数据流之间的依赖关系,可以为后续进一步开展形式化验证提供支持。将系统工具应用于真实的航天嵌入式软件需求中,通过时序偏离检测分析及需求完整性验证,表明本工具可有效帮助需求人员发现和改进时序偏离和需求分解不一致等问题。

关键词： marte 嵌入式软件时序分析梯度下降算法需求完整性验证

基于marte的面向时间方面建模及转换研究

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于MARTE的面向时间方面建模及转换研究

作者：孙晴晴南京大学

学位级别：硕士

随着计算机系统应用的不断普及和深入,软件系统开发的复杂度和规模也在不断增加。为了控制和解决这一问题,人们提出了模块化的开发理念,实践证明这是降低软件开发复杂度的有效方法。模型驱动的开发将平台无关模型（PIM）和平台有关模型... 详细信息

随着计算机系统应用的不断普及和深入,软件系统开发的复杂度和规模也在不断增加。为了控制和解决这一问题,人们提出了模块化的开发理念,实践证明这是降低软件开发复杂度的有效方法。模型驱动的开发将平台无关模型（PIM）和平台有关模型（PSM）分离,并支持PIM根据不同平台到PSM的转换和代码生成。模型驱动的方法将业务逻辑处理提升到更高的抽象层次,有效的支持软件开发过程中模块的划分,提高了代码复用率。实时和嵌入式系统是一类软件和硬件构成的异质系统,其系统计算的正确性依赖于不同事件之间的时间间隔。实时系统中的时间约束与基本功能行为之间通常存在正交的耦合关系,横切多个功能模块,难以封装成独立单元进行开发。为了解决非功能属性破坏系统模块化特性的问题,本文以实时和嵌入式系统中的时间约束为原型,尝试模型驱动的开发理念,使用面向方面建模技术,将时间约束和系统行为分开建模和设计。将模型驱动的方法应用到实时系统中,既要考虑一般的功能性业务逻辑模型,还要对广泛存在的时间约束、资源分配等非功能属性进行建模。针对实时系统,将行为建模和时间建模分开进行,本文主要做了以下几方面的工作： 1.基于marte建模语言对时间建模 marte建模语言是OMG发布的实时系统建模和分析语言,作为UML的轻量级扩展,marte取代了之前的SPT （Schedulability, Performance and Time）标准,成为实时建模领域的正式规约。marte规范中使用离散时间和连续时间两种方式模拟现实世界的时间,提供了诸如Clock、 ClockType和Clock Constraints等大量的时间建模元素,丰富了时间模型语义,支持实时和嵌入式系统的时间特性描述。基于marte语言,本文根据不同的系统需求,选取其中合适的建模元素,对系统中的时间约束进行建模。 2.面向方面的时间建模技术面向方面的建模方法强调关注点分离的技术,在软件开发的早期识别横切行为及其横切的方式,将其进行模块化单独建模,解决了面向对象技术经常引起的代码缠结和代码分散的问题。Theme方法,是面向方面的分析与设计的一种典型方法,提供了面向方面的关注点分离和方面编织技术,本文扩展了Theme方法,基于marte建模语言,提出了一种面向方面的时间建模技术,将时间作为横切关注点,在系统的开发初期识别系统中的一般行为和时间约束行为,并确定时间约束行为和系统其他行为之间的关系,按照关注点分离的原则,将一般行为和横切行为单独进行建模。最后将得到的一般关注点模型和方面模型采用面向方面的编织技术进行整合,形成完整的系统模型。 3.时间方面模型到SystemC模型的转换和系统仿真模型驱动的一个重要目标是根据模型,使用模型转换技术自动或半自动的生成系统可执行代码。模型转换也是模型驱动过程中的最核心技术之一,在完成建模的基础上,本文继续了模型转换和系统仿真相关的研究。模型的仿真有助于迭代构造高质量的可信模型。本文根据得到的时间方面模型,构造映射规则,将marte模型转换到具有软硬件协同建模和分析能力的SystemC语言模型,并使用相关工具,从SystemC模型生成代码,为对系统中的时间约束进行仿真验证提供支持。

关键词：模块化模型驱动 marte 时间面向方面横切转换

基于marte的IMA系统时间资源可调度配置验证

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

电子世界 2016年第4期 183-184页

作者：程桢南京航空航天大学计算机科学与技术学院

目前综合模块化航空电子系统(IMA)在资源配置方面有非常高的安全可靠性需求,其中时间资源的可调度性配置验证也显得至关重要。本文在AFDX网络架构下提出了一种IMA系统时间相关概念的marte建模和时间资源可调度配置的正确性验证方法。建... 详细信息

目前综合模块化航空电子系统(IMA)在资源配置方面有非常高的安全可靠性需求,其中时间资源的可调度性配置验证也显得至关重要。本文在AFDX网络架构下提出了一种IMA系统时间相关概念的marte建模和时间资源可调度配置的正确性验证方法。建立了IMA系统通信虚拟链路、AFDX终端、分区以及进程等相关元素到marte模型元素的建模规则,并设计了基于可调度分析工具MAST的时间资源可调度配置验证框架,最后利用相关实例进行仿真和分析得到验证结果。

关键词：综合航电系统模型驱动工程 marte 系统资源配置

在线全文

学校读者我要写书评

暂无评论

新改型的marte导弹

空天技术 1987年第11期 59-60页

作者：邢娅

直升飞机发射的marte MK2中程反舰导弹现正在奥托·梅拉腊公司批生产,1986年上半年该公司接受了意大利空军(代表意大利海军)的第一批约50枚导弹及6套发射系统的生产合同。预定于1987年内交付的这些导弹中将包括一定数量的用于验收试验... 详细信息

直升飞机发射的marte MK2中程反舰导弹现正在奥托·梅拉腊公司批生产,1986年上半年该公司接受了意大利空军(代表意大利海军)的第一批约50枚导弹及6套发射系统的生产合同。预定于1987年内交付的这些导弹中将包括一定数量的用于验收试验的导弹。发射系统将安装在SH—3D直升飞机上,那些飞机很可能装载在Giuseppe Garibaldi直升机母舰上。奥托公司认为,marte是介于本公司的远程“重”型导弹如Otomat及英国的海鸥和法国的AS15·TT导弹之间的一种中型武器。尽管一架中型直升飞机只能带两枚Ma-

关键词：导弹空军意大利军队南欧 marte 舰艇发射

基于UML marte处理AADL的端到端流延迟

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

软件工程师 2015年第11期 24-26页

作者：杨夏湖南科技职业学院湖南长沙410004

AADL和marte都支持对实时嵌入式系统形式化建模的分析。利用marte的时间模型设备,研究marte是如何对实时嵌入式系统的建模和分析的,能够比较准确的通过事件或者数据端口的端到端流延迟分析,表达AADL周期性或非周期性任务。

关键词： AADL marte 流延迟

在线全文

学校读者我要写书评

暂无评论

智利北部marte斑岩金矿床

世界核地质科学 1993年第3期 289-289页

作者：缪卫东

marte首次证实了一个斑岩金矿床,它位于智利北部Andean Cordillera的Maricunga带上。从1981—1987年进行勘探,圈定了66t的金储量。1989年后期,此矿床投入生产,采用露天开采,堆浸操作。此金矿床是一个线性钙碱性深成火山弧的一部分,其形... 详细信息

marte首次证实了一个斑岩金矿床,它位于智利北部Andean Cordillera的Maricunga带上。从1981—1987年进行勘探,圈定了66t的金储量。1989年后期,此矿床投入生产,采用露天开采,堆浸操作。此金矿床是一个线性钙碱性深成火山弧的一部分,其形成于中—晚中新世,当向东方向的俯冲作用消减时,矿床及其周围下面的大陆基底的随后挤压造成一系列高角度逆断层。岩侏侵位和金矿化发生在13—

关键词：斑岩金矿泥质盖层金矿床贵金属矿床 marte 智利