0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看威廉希尔官方网站 视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示

Ravenscar Ada任务和FACE安全配置文件

星星科技指导员 来源:嵌入式计算设计 作者:BENJAMIN BROSGOL,DR 2022-11-09 14:49 次阅读

作者:BENJAMIN BROSGOL,DR. DUDREY SMITH,DR. PATRICK ROGERS

需要占用空间小或必须符合行业保证标准(如 DO-178B或 DO-178C)的机载系统对运行时支持库中的尺寸和复杂性成本很敏感。为了满足这些需求,未来机载能力环境(FACE?威廉希尔官方网站 标准已将 Ada 编程语言任务功能的 Ravenscar 子集指定为必须满足安全和/或安全保证要求的软件组件的可接受并发方法之一。

FACE方法是一种政府-行业软件标准和商业战略,旨在获得价格合理的软件系统,在全球国防项目中快速集成便携式功能,并吸引创新并快速且经济地部署。它通过通用参考体系结构上下文中定义良好的标准接口促进组件可移植性和重用性。参考体系结构包括一个操作系统段 (OSS),它提供应用程序可能需要的运行时服务。OSS 对 FACE 组件的支持的通用性取决于组件的配置文件,该配置文件是基于性能、安全和/或安全性要求的完整 FACE 功能的子集。FACE威廉希尔官方网站 标准定义了几个配置文件:

通用(根据需要保证,不保证确定性,可选时间分区,需要空间分区)

安全性(安全/安保保证、确定性和时间/空间划分)

安全(安全保证、确定性和时间/空间划分)——基础和扩展

与这些配置文件对应的是 C、C++、Ada 和 Java 的语言子集(“功能集”)。功能集定义了允许哪些功能,禁止哪些功能:允许确保足够的表现力,禁止有助于根据相关保证要求简化分析/认证。运行时支持库必须实现允许的功能,并且可能提供更多功能,但(对于安全功能集)以确保确定性并促进保证分析的方式。

FACE威廉希尔官方网站 标准为Ada定义了几个功能集:

Ada 95 安全 – Ada 95 安全基础和安保以及 Ada 95 安全扩展

Ada 95 通用型

Ada 2012 通用

这些配置文件以两种方式支持并发:通过操作系统环境(POSIX 或 ARINC 653)中的线程 API,或通过语言构造(任务)。

使用语言中定义的并发功能具有源代码可移植性的优势,因为每个 Ada 实现都需要支持 Ada 任务模型。Ada任务的高级性质也倾向于提高可靠性,因为程序员可以直接表达典型的通信范式,而不是通过信号量或条件变量等较低级别的结构。

允许的任务功能在通用和安全功能集之间有所不同。对于通用集,几乎允许使用完整的 Ada 任务功能。但是,在需要安全或安全保证的情况下,运行时支持的复杂性将是有问题的,并且由于实现依赖性,完整模型还引入了应用程序非确定性。

需要任务功能的确定性子集。该子集需要具有足够的表现力,以便对现实世界的航空电子应用程序进行编程,并且还需要足够简单以高效实施。它应该有助于静态分析,以验证关键属性,包括硬实时系统的可调度性(确保满足所有截止日期),并支持根据保证标准进行认证。Ravenscar任务子集是专门为满足这些目标而设计的,并且由FACE安全功能集允许;它是 Ada 95 任务功能的一个子集,是 Ada 2005 语言标准的一部分。

艾达任务和乌鸦限制

并发 Ada 程序由一组任务(控制线程)组成,这些任务通过称为会合的任务间通信设施直接相互通信,或通过共享数据间接通信。对于后一个目的,该语言提供了一种称为受保护对象的高级机制,用于基于状态/条件的互斥,同时避免竞争条件和死锁。其他形式的安全数据共享也由语言定义,例如依赖于硬件强制的访问原子性。

Ada 任务模型包括用于终止任务的功能(例如,中止语句)、与时间相关的支持(例如相对和绝对延迟)和具有实时时钟操作的包,以及基于事件或超时的异步机制。为了防止数据损坏,某些代码节被定义为中止延迟,并且需要在异步终止之前执行到完成。

任务和受保护对象可以全局定义,也可以在本地范围内定义;语义防止悬而未决的引用(例如,子程序在其所有本地任务终止之前不允许返回)。

任务可以在多个处理器/内核上以实际并行方式执行,也可以在单个处理器/内核上的调度程序控制下多路复用。可以为任务分配优先级,无论是静态的还是动态的,并且根据任务调度策略,当多个任务有资格执行时,在程序执行期间的不同时间点考虑优先级。

图 1 显示了一个 Ada 任务程序的简单示例,该程序具有两个任务(读取器和写入器),通过受保护的数据对象(资源)进行互斥通信。

图1:Ada任务程序的示例,其中读取器和编写器通过资源进行通信。

21

完整的任务模型具有很强的表现力,但需要复杂的运行时实现。为了支持Ada中的高效,高完整性的并发应用程序,特别是那些具有硬实时要求的应用程序,1997年和1999年在英国Ravenscar举行的研讨会指定了一组限制,允许任务程序在其功能和时间属性方面进行静态分析。这个子集被称为Ravenscar Profile;为了避免与“轮廓”的FACE概念混淆,这里将其称为Ravenscar子集。

遵循 Ravenscar 子集限制的程序具有以下几个属性:它包含固定数量的非终止任务,所有任务都是全局定义的;每个任务都有一个触发事件,要么基于时间,要么基于事件(从另一个任务或环境发出信号),触发事件的发生次数可能不受限制;唯一的任务交互是通过共享/受保护的数据对象。

这些限制是通过标准 Ada 语言功能定义的,特别是实现强制执行的一系列编译指示。两个这样的编译指示任务调度和对象锁定策略:

杂注Task_Dispatching_Policy (FIFO_Within_Priorities)

杂注Locking_Policy (Ceiling_Locking)

这些策略有助于调度性分析方法,如速率单调分析 [5],并有助于最小化优先级倒置,防止基于互斥的死锁,并保证任务始终满足其截止日期(有关进一步说明,请参阅侧栏)。

Ravenscar的其他限制是对特定语言功能的限制。其中包括禁止相对延迟语句(因为它们不是必需的,也不能可靠地用于实现周期性)、中止语句、本地定义的任务或受保护的对象、任务集合、动态优先级、任务分配和异步控制转移。简化实现或促进可调度性分析的其他限制包括每个受保护对象最多一个队列(条目)的限制,在任何给定时间最多有一个调用方挂起,以及禁止任务终止。Ravenscar子集的完整定义出现在Ada 2012标准[6]中。

虽然具有限制性,但 Ravenscar 子集也足够通用,可以表达一系列有用的任务习语,例如循环(周期性)任务;事件驱动(非定期或零星)任务、中断处理程序和共享资源(简单的受保护对象)。

图 2 显示了图 1 中读取器/写入器示例变体中的 Ravenscar 子集,其中包含避免漂移的循环(周期性)任务。

图2:图 1 中示例变体中的 Ravenscar 子集。

22

在 FACE 上下文中实现 Ravenscar 任务子集

除了允许 Ravenscar 子集外,Ada 95 安全功能集还允许或禁止各种顺序语言功能。例如,安全基础功能集允许中断支持、具有单个默认处理程序的预定义异常以及来自 Ada 预定义环境的某些包,同时禁止动态分配。Ada 95安全扩展功能集通常允许异常处理,并允许在启动时动态分配,同时禁止释放。

为任一安全功能集实现运行时支持库的挑战在于,如何以有助于分析相关保证要求的方式提供允许的功能。满足这一挑战的实现的一个示例是AdaCore的Ravenscar-Cert库,它支持安全基础和安全扩展功能集中允许的所有功能,并满足DO-178B或DO-178C中的适用目标。该库实现了 Ravenscar 任务功能、异常传播、最后机会处理程序和返回不受约束数组的函数的标记/发布机制(不需要堆管理)。Ravenscar-Cert库已经为Wind River的VxWorks 653和Lynx Software Technologies的LynxOS-178 RTOSes实现。此库中的 Ravenscar 任务支持小于 40 KB。

迎接挑战

并发编程对于设计和实现实时嵌入式应用程序,特别是FACE组件非常有用,但它带来了重大的软件工程挑战:

•可移植性。Ravenscar 子集由 Ada 语言标准定义,其限制集可以帮助保证确定性行为。遵循Ravenscar子集的程序(以及对实现相关功能的其他限制)将跨不同的实现和平台移植,这是FACE方法的主要目标。Ada的Ravenscar任务子集可以帮助应对这些挑战。

•可靠性。对于实时程序,可靠性不仅意味着功能正确性(计算正确的结果),还意味着时间可预测性(满足严格的截止日期)。Ravenscar 子集有助于以多种方式实现这些要求。禁止异步等复杂功能,允许的任务间通信的简单形式适用于静态分析,队列限制有助于计算最坏情况执行时间。Ravenscar 限制指定的任务调度和对象锁定策略同样有助于调度分析,并产生比传统循环执行更简单、更易于维护的体系结构。

•效率。由于没有语义复杂性,因此可以实现“精益和平均”的运行时实现。不需要支持任务终止、队列管理和动态优先级等功能,并且正如 AdaCore 的 Ravenscar-Cert 库等实现所证明的那样,所需的功能可以有效地映射到底层实时操作系统提供的服务。

审核编辑:郭婷

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 操作系统
    +关注

    关注

    37

    文章

    6808

    浏览量

    123291
  • C++
    C++
    +关注

    关注

    22

    文章

    2108

    浏览量

    73624
  • 读取器
    +关注

    关注

    0

    文章

    46

    浏览量

    5238
收藏 人收藏

    评论

    相关推荐

    linux网卡配置文件

    网卡配置文件     网卡目录[root@localhost opt]# ls /etc/sysconfig/network-scripts/网卡文件名字,和我们ifconfig看到的一样
    的头像 发表于 12-10 10:09 206次阅读

    springboot的项目如何既要用jar包启动,同时还可以为不同的机房设置不同的配置文件

    作者:京东科技 李意文 1、首先先把配置文件从jar中抽离 示例代码:   org.apache.maven.plugins maven-jar-plugin 3.2.0
    的头像 发表于 10-19 16:48 504次阅读
    springboot的项目如何既要用jar包启动,同时还可以为不同的机房设置不同的<b class='flag-5'>配置文件</b>

    HID over GATT配置文件(HOGP)低功耗蓝牙

    电子发烧友网站提供《HID over GATT配置文件(HOGP)低功耗蓝牙.pdf》资料免费下载
    发表于 09-26 11:01 1次下载
    HID over GATT<b class='flag-5'>配置文件</b>(HOGP)低功耗蓝牙

    确定LDO的任务配置文件兼容性

    电子发烧友网站提供《确定LDO的任务配置文件兼容性.pdf》资料免费下载
    发表于 09-24 10:44 0次下载
    确定LDO的<b class='flag-5'>任务</b><b class='flag-5'>配置文件</b>兼容性

    InModbus2配置文件的注意事项

    大家好,由于最近经常有人问我InModbus2的配置文件如何编辑来达到想要的结果,所以发布一些关于InModbus2的配置文件注意事项,后期我还会发布一些示例来供大家参考让大家都掌握一些简单
    发表于 07-26 07:21

    如何完成编辑配置文件来采集数据

    今天通过给大家做一个路由器采集PLC地址为00001数据类型为bit的寄存器数值的配置文件来介绍一下如何完成编辑配置文件来采集数据。controllers:- controller:id
    发表于 07-26 06:50

    鸿蒙开发Ability Kit程序框架服务:FA模型应用配置文件

    应用配置文件中包含应用配置信息、应用组件信息、权限信息、开发者自定义信息等,这些信息在编译构建、分发和运行解决分别提供给编译工具、应用市场和操作系统使用。
    的头像 发表于 06-24 14:49 355次阅读
    鸿蒙开发Ability Kit程序框架服务:FA模型应用<b class='flag-5'>配置文件</b>

    鸿蒙开发:【Stage模型应用配置文件

    应用配置文件中包含应用配置信息、应用组件信息、权限信息、开发者自定义信息等,这些信息在编译构建、分发和运行解决分别提供给编译工具、应用市场和操作系统使用。
    的头像 发表于 06-15 09:15 1666次阅读
    鸿蒙开发:【Stage模型应用<b class='flag-5'>配置文件</b>】

    鸿蒙开发:任务(Mission)与启动模式

    如前文所述,一个UIAbility实例对应一个任务。UIAbility实例个数与UIAbility配置的启动模式有关。在FA模型下,通过config.json配置文件中的“launchType”属性
    的头像 发表于 06-14 11:31 473次阅读
    鸿蒙开发:<b class='flag-5'>任务</b>(Mission)与启动模式

    CYW4373是否支持SPP和GATT配置文件

    CYW4373 是否支持 SPP 和 GATT 配置文件
    发表于 05-31 06:13

    鸿蒙OpenHarmony:【配置代理】

    新建代理配置文件
    的头像 发表于 04-29 22:17 813次阅读
    鸿蒙OpenHarmony:【<b class='flag-5'>配置</b>代理】

    支持CiA402驱动器配置文件的示例程序用于通过EtherCAT®通信进行电机控制

    电子发烧友网站提供《支持CiA402驱动器配置文件的示例程序用于通过EtherCAT®通信进行电机控制.pdf》资料免费下载
    发表于 02-21 14:21 2次下载
    支持CiA402驱动器<b class='flag-5'>配置文件</b>的示例程序用于通过EtherCAT®通信进行电机控制

    Linux系统中的配置文件

    系统文件,用于配置主机名与 IP 地址的映射关系。当系统需要解析主机名时,会首先查找 /etc/hosts 文件,如果在该文件中找到了相应的映射关系,则直接使用对应的 IP 地址进行通
    发表于 02-19 17:36 1221次阅读

    labview生成exe文件如何配置文件

    可执行文件之前,您需要确保正确配置文件,以便应用程序能够在不同计算机上正确运行。 下面是一个详尽、详实、细致的步骤指南,告诉您如何配置LabVIEW生成的可执行文件: 确保您的应用程序
    的头像 发表于 12-27 16:28 2183次阅读

    labview的opc生成配置文件

    的数据交互和通信。在 LabVIEW 中生成 OPC 配置文件有助于实现与其他设备的数据传输和共享,本文将详细介绍如何生成 OPC 配置文件。 首先,在 LabVIEW 中生成 OPC 配置文件,我们
    的头像 发表于 12-26 17:57 1866次阅读