色哟哟视频在线观看-色哟哟视频在线-色哟哟欧美15最新在线-色哟哟免费在线观看-国产l精品国产亚洲区在线观看-国产l精品国产亚洲区久久

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

    文章

    6850

    瀏覽量

    123429
  • C++
    C++
    +關注

    關注

    22

    文章

    2112

    瀏覽量

    73706
  • 讀取器
    +關注

    關注

    0

    文章

    47

    瀏覽量

    5286
收藏 人收藏

    評論

    相關推薦

    linux網卡配置文件

    網卡配置文件 ? ? 網卡目錄[root@localhost opt]# ls /etc/sysconfig/network-scripts/網卡文件名字,和我們ifconfig看到的一樣
    的頭像 發表于 12-10 10:09 ?244次閱讀

    TAS5711用GDE生成的EQ cfg配置文件怎么加載到單片機上?

    TAS5711 的用GDE 生成的EQcfg配置文件怎么加載到單片機上。
    發表于 10-25 13:48

    springboot的項目如何既要用jar包啟動,同時還可以為不同的機房設置不同的配置文件

    作者:京東科技 李意文 1、首先先把配置文件從jar中抽離 示例代碼: ? org.apache.maven.plugins maven-jar-plugin 3.2.0
    的頭像 發表于 10-19 16:48 ?539次閱讀
    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 ?373次閱讀
    鴻蒙開發Ability Kit程序框架服務:FA模型應用<b class='flag-5'>配置文件</b>

    鴻蒙開發:【Stage模型應用配置文件

    應用配置文件中包含應用配置信息、應用組件信息、權限信息、開發者自定義信息等,這些信息在編譯構建、分發和運行解決分別提供給編譯工具、應用市場和操作系統使用。
    的頭像 發表于 06-15 09:15 ?1711次閱讀
    鴻蒙開發:【Stage模型應用<b class='flag-5'>配置文件</b>】

    鴻蒙開發:任務(Mission)與啟動模式

    如前文所述,一個UIAbility實例對應一個任務。UIAbility實例個數與UIAbility配置的啟動模式有關。在FA模型下,通過config.json配置文件中的“launchType”屬性
    的頭像 發表于 06-14 11:31 ?509次閱讀
    鴻蒙開發:<b class='flag-5'>任務</b>(Mission)與啟動模式

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

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

    哪些芯片支持藍牙經典A2DP配置文件和LE音頻?

    哪些芯片支持藍牙經典 A2DP 配置文件和 LE 音頻?
    發表于 05-24 07:17

    鴻蒙OpenHarmony:【配置代理】

    新建代理配置文件
    的頭像 發表于 04-29 22:17 ?834次閱讀
    鴻蒙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 ?1328次閱讀
    主站蜘蛛池模板: 使劲别停好大好深好爽动态图| 麻豆区蜜芽区| 秋霞电影院午夜伦高清| 亚洲国产欧美国产综合在线| 超碰97人人做人人爱少妇| 免费观看a视频| 中文字幕在线观看国产| 久久精品熟女亚洲AV国产| 野花日本大全免费高清完整版| 国产在线观看www| 亚洲精品国产第一区第二区| 国产亚洲视频在线观看| 亚洲第一综合天堂另类专| 国产真实女人一级毛片| 亚洲成 人a影院青久在线观看| 国产精品爽爽久久久久久蜜桃网站| 神马伦理不卡午夜电影| 国产精品成人A蜜柚在线观看| 受被攻做到腿发颤高h文| 国产成人在线视频| 午夜影院美女| 精品国产mmd在线观看| 欧美色妞AV重囗味视频| 99在线视频免费观看视频| 欧美男女爱爱| 国产AV精品久久久免费看| 天堂色| 国产美女又黄又爽又色视频网站| 亚洲国产货青视觉盛宴| 久久久久夜| jizzjizz中国大学生| 色老汉网址导航| 好湿好滑好硬好爽好深视频| 在线 无码 中文 强 乱| 欧美白人极品性喷潮| 成人影片迅雷下载| 亚洲高清有码中文字| 快播h动漫网站| 纯肉腐文高H总受男男| 羞羞漫画在线播放| 久久资源365|