文献

J-GLOBAL ID：201902272565579816   整理番号：19A1355849

SpaceOSにおけるいくつかの大域的性質の形式的記述と検証【JST・京大機械翻訳】

Formalization and Verification of Several Global Properties of SpaceOS

著者 (4件)： Gu Haibo (中国科学技術大学 計算机科学与技術学院,合肥230027;中国科学技術大学 蘇州研究院軟件安全実験室,江蘇 蘇州215123) ,  Fu Ming (中国科学技術大学 蘇州研究院軟件安全実験室,江蘇 蘇州215123;華為上海研究所2012実験室-OS内核実験室,上海201206) ,  Qiao Lei (北京控制工程研究所,北京,100190) ,  Feng Xinyu (中国科学技術大学 蘇州研究院軟件安全実験室,江蘇 蘇州215123;南京大学 計算机軟件新技術国家重点実験室,南京210023)
資料名： Xiaoxing Weixing Jisuanji Xitong  (Xiaoxing Weixing Jisuanji Xitong)
巻： 40  号： 1  ページ： 141-148  発行年： 2019年 
JST資料番号： C2136A  ISSN： 1000-1220  CODEN： XWJXEH  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： SpaceOSは北京制御工学研究所が自主に開発した組込み式リアルタイムオペレーティングシステムであり、すでに月工学、宇宙ステーションなどの重大な宇宙プロジェクトに応用されている。SpaceOSは,低レベルのシステムソフトウェアとして,宇宙ミッションの成功に影響する重要な要素である。SpaceOSは,いくつかのカーネルモジュール(例えば,タスク管理,スケジューリング,通信,および時間管理など)の協調プロセスに要求されるグローバル特性を提示した。本論文では,既存のオペレーティングシステム検証フレームワークのグローバル性質の推論を拡大し,SpaceOSカーネルに抽象モデルを作り,主要なシステムコールの抽象仕様を与え,設計要求に基づいて形式的定義を与え,いくつかの大域的特性を記述する。厳格な数学的証明により、SpaceOSが抽象設計レベルでこれらの大域的性質を満たすことを保証した。すべての仕事は助手Coqで完成することを証明した。Data from Wanfang. Translated by JST.【JST・京大機械翻訳】

シソーラス用語： システムプログラム ,  形式記述 ,  宇宙ステーション ,  モデル ,  宇宙空間 ,  *オペレーティングシステム ,  スケジューリング
準シソーラス用語： システムコール ,  時間管理 ,  タスク管理 ,  リアルタイムOS ,  制御工学 ,  北京市 , 【Automatic Indexing@JST】

分類 (4件)： 計算機網  (JC03000K) ,  人工知能  (JE08000Z) ,  システム設計・解析  (IA02030D) ,  計算機シミュレーション  (JE11000H)

タイトルに関連する用語 (3件)： 性質 ,  形式的記述 ,  検証