基于时间自动机的AADL端到端流规约验证方法

体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具,可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而,AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果,尤其是对于资源动态分配的实时系统。为解决结果不精确的问题,可结合基于系统有穷状态空间遍历的模型检验方法。首先,将实时系统AADL模型转换为时间自动机(TA)模型,以TA为理论体系进行模型检验。其次,基于反应链的需求分类定义端到端延迟需求表达模式。最后,给出对应需求模式的观察者模型,与系统模型并行组合,优化模型验证的时空资源消耗。     

基于EDF调度算法的端到端延迟保证方法

EDF(EarliestDeadlineFirst)是一种高效的调度算法。为了将其应用于提供端到端延迟保证,提出了一种新的算法JT-EDF(JitterTunableEDF),并证明了所有的端到端EDF调度算法都可以在相同的条件下保证相同的端到端延迟界。     

基于抖动测试的AFDX端到端延迟紧性修正

AFDX引入虚拟链路(Virtual Link)实现物理带宽资源的逻辑分隔。由于数据帧的异步到达和多路复用输出造成虚拟链路的时延抖动现象,并最终导致流量端到端延迟分析的不确定性。本文提出了一种基于抖动测试值的网络演算紧缩方法。通过分布式测试,获得虚拟链路在网络中的实际传输抖动,并以此为基础,建立了流量传输精确化模型,通过流量模型的逐级修正,使端到端延迟计算结果逐级精确化。通过将抖动实际值与理论分析结果相结合,提供了网络演算悲观度及其扩散影响度量的直观对比,提高了延迟计算的紧性。     

基于IP的端到端实时节目流播放系统

针对IP网上的实时多媒体应用，提出了利用MPEG-4标准码流在带宽有限条件下综合运用多种传输标准和协议来实现具有有一定服务质量保证的端到端的实时节目流播放系统。     

基于XML的UML模型向AADL模型的自动转换

UML已经成为复杂系统建模的工业标准,并可借助代码自动生成工具实现从分析到编码的开发过程自动化;AADL具有精确的语义和严格的语法规范,可用于描述嵌入式实时系统的软、硬件体系结构,并能分析系统的功能及非功能属性。 UML和AADL模型的基本元对象有相互对应关系,并且两种模型的表示都能够采用标准的XML的交换格式。为充分发挥两种语言的优势,文中研究了UML模型向AADL模型的自动转换,以XML为媒介实现两种模型的元对象的对应转换,最终达到两种模型的转换,使用户在设计阶段能够结合运用AADL、UML工具的优点对系统进行分析。     

WSN中单数据流端到端延迟上界研究

在WSN中采用独立分析（SFA）法求得的单数据流端到端延迟上界有时比整体分析（TFA）法求得的总数据流端到端延迟上界要大, 这不符合物理意义。针对这一问题, 分析了现有TFA法与SFA法在数据流服务分配机制上的差别, 并指出这两种方法求得的延迟上界不具有可比性。随后在修正流经节点数据流输出上界的基础上, 推导出与TFA法数据流服务分配机制相匹配的单数据流端到端延迟上界表达式。公式推导与数值分析结果均表明, 本方法求得的单数据流端到端延迟上界能够被TFA法总数据流端到端延迟上界所包络, 符合物理意义且更精确。     

抗干扰通信网端到端延迟上界仿真分析

考虑到通信网端到端的延迟抖动模式,为了降低数据传输耗时,进行抗干扰通信网端到端延迟上界仿真分析.根据MAC层中协议,计算抗干扰通信网端到端延迟,确定上界以及通信网端到端延迟抖动上界,在通信网式中模型中,引入漂移因子,完成通信网端到端延迟上界演算过程,实现抗干扰通信网端到端延迟上界仿真分析.仿真结果表明,上述方法的数据传...     

基于模型的嵌入式系统软件工程语言AADL与UML的比较

随着嵌入式系统规模、复杂度和性能需求的提升,嵌入式系统开发的重点从代码级提前到模型级,模型驱动体系结构成为嵌入式系统开发的主流。统一建模语言（uML）和结构分析和设计语言（AADL）是模型驱动系统工程的标准,从方法、扩展机制和应用领域三个方面对两者进行研究和比较,讨论模型分析、模型转换等相关技术。最后,探讨了UML和AADL的发展与研究方向     

基于网络演算计算保证服务端到端延迟上界

归纳总结了网络演算,阐明了网络演算的两个基本工具——进入曲线和服务曲线,得出了服务曲线存在瓶颈效应、端到端延迟的理想与近似确定性上界、提供保证服务网络节点的服务曲线需求等结论,计算了服务曲线以速率等待时间及PGPS(packetizedgeneralizedprocessorsharing)形式表示的保证服务端到端延迟确定性上界.     

一种基于支持向量回归的互联网端到端延迟预测算法

互联网端到端延迟是指IP分组沿着互联网中一条确定路径进行传输的延迟,端到端延迟的精确预测是大量网络活动的基础,从网络协议设计到网络监测,再从确保端到端QoS性能到各种实时业务性能提升。提出一种新的端到端延迟的预测方法,主要贡献有:a)将互联网端到端延迟预测的问题转换为多元回归的预测问题,提出了基于多元回归的端到端延迟预测框架;b)采用支持向量回归SVR方法来求解端到端延迟的多元回归问题,提出了基于SVR的互联网端到端延迟预测算法。最后使用互联网采集的RTT数据来验证提出的算法,实验结果表明,提出的预测算法具有快速和精确特点,是一种适合实际应用的预测算法。     

Clock constraint specification language: specifying clock constraints with UML/MARTE

The Object Management Group (OMG) unified modeling language (UML) profile for modeling and analysis of real-time and embedded systems (MARTE) aims at using the general-purpose modeling language UML in the domain of real-time and embedded (RTE) systems. To achieve this goal, it is absolutely required to introduce inside the mainly untimed UML an unambiguous time structure which MARTE model elements can rely on to build precise models amenable to formal analysis. The MARTE Time model has defined such a structure. We have also defined a non-normative concrete syntax called the clock constraint specification language (CCSL) to demonstrate what can be done based on this structure. This paper gives a brief overview of this syntax and its formal semantics, and shows how existing UML model elements can be used to apply this syntax in a graphical way and benefit from the semantics.     

Hybrid MARTE statecharts

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 specification and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to extend 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 variables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition systems 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.     

The COMPLEX methodology for UML/MARTE Modeling and design space exploration of embedded systems

The design of embedded systems is being challenged by their growing complexity and tight performance requirements. This paper presents the COMPLEX UML/MARTE Design Space Exploration methodology, an approach based on a novel combination of Model Driven Engineering (MDE), Electronic System Level (ESL) and design exploration technologies. The proposed framework enables capturing the set of possible design solutions, that is, the design space, in an abstract, standard and graphical way by relying on UML and the standard MARTE profile. From that UML/MARTE based model, the automated generation framework proposed produces an executable, configurable and fast performance model which includes functional code of the application components. This generated model integrates an XML-based interface for communication with the tool which steers the exploration. This way, the DSE loop iterations are efficiently performed, without user intervention, avoiding slow manual editions, or regeneration of the performance model. The novel DSE suited modelling features of the methodology are shown in detail. The paper also presents the performance model generation framework, including the enhancements with regard the previous simulation and estimation technology, and the exploration technology. The paper uses an EFR vocoder system example for showing the methodology and for demonstrative results.     

Towards formalising AADL in Proof Assistants

This paper presents first steps towards a formalisation of the Architecture Analysis and Design Language, mainly concentrating on a representation of its data model. For this, we contrast two approaches: one set-based (using the B modelling framework) and one in a higher-order logic (using the Isabelle proof assistant). We illustrate a transformation on a simplified part of the AADL metamodel concerning flows.     

基于MARTE模型的系统可靠性预测

系统的可靠性是系统的重要非功能属性之一。传统的可靠性分析在系统开发结束后进行,可能会发现由于系统开发早期的架构设计不合理而导致的问题,这时再修改系统架构并重做后继开发步骤,将会浪费大量人力和物力。如果能在开发的早期阶段,在系统模型层面进行分析并预测,则可以尽早地发现系统可靠性方面的问题并将其修复。UML是一种通用的、标准化的建模语言,MARTE是UML在嵌入式实时系统领域的扩展。提出了基于MARTE模型的系统可靠性预测方法,该方法考虑的MARTE模型包括用例图、活动图、部署图。先将MARTE模型转换为马尔可夫决策过程网络模型,再利用概率模型检测工具PRISM进行分析,得到系统可靠性的预测结果。实例研究表明,所提方法不仅能够预测系统可靠性的最大值和最小值,还能通过调整各个资源的可靠性值,考察其对系统可靠性的影响,为设计人员的进一步工作提供参考。     

AADL模型的测试方法研究

近几年来,MDA开发方式的应用使得如何保证模型质量成为研究的热点.以基于模型的测试为研究对象,研究了对AADL模型进行模型测试的方法,并提出了结合马尔可夫链对AADL模型进行测试的框架以及实施方法.最后,通过示例进一步说明了该方法.     

基于时间Petri网的AADL模型

随着嵌入式系统设计日益复杂,对系统的描述也提出了越来越高的要求,特别是实时性能。因此如何描述实时性能逐渐受到重视。在嵌入式系统中,线程的时间属性影响着系统的实时性,因此在设计早期利用AADL描述线程,但是AADL只是一种半形式化的语言,不够精确,并可能产生二义性。因此,把AADL模型转化为时间Pe砸网,但是时间Petri网不能很好地表示AADL的时间属性。故在研究AADL模型的时间属性的基础上,针对时间Petri考虑区域值延时与固定延时,并把固定延时当作区域值时延的一种特殊情况。最后给出针对AADL模型转化为时间Petri网的相应规则。