文献

J-GLOBAL ID：201602205402920090   整理番号：16A0032993

PRISMに基づく分散型実時間オペレーティングシステムタスクスケジューリングの形式的検証【Powered by NICT】

Formal Verification of Distributed Real-time Operating System Task Scheduling Based on PRISM

著者 (6件)： Huo Yanyan (Beijing Key Lab. of Electronic System Reliability Technol.,Capital Normal Univ., Beijing) ,  Guan Yong (Beijing Key Lab. of Electronic System Reliability Technol.,Capital Normal Univ., Beijing) ,  Li Xiaojuan (Beijing Key Lab. of Electronic System Reliability Technol.,Capital Normal Univ., Beijing) ,  Wang Rui (Beijing Key Lab. of Electronic System Reliability Technol.,Capital Normal Univ., Beijing) ,  Zhang Jie (Coll. of Information Sci. & Technol.,Beijing Univ. of Chemical Technol., Beijing) ,  Wei Hongxing (School of Mechanical Engineering and Automation,Beijing Univ. of Aeronautics & Astronautics, Beijing)
資料名： Xiaoxing Weixing Jisuanji Xitong  (Xiaoxing Weixing Jisuanji Xitong)
巻： 36  号： 9  ページ： 2125-2129  発行年： 2015年 
JST資料番号： C2136A  ISSN： 1000-1220  CODEN： XWJXEH  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： 大規模の急速な発展は,回路技術を統合し,迅速な開発の波とコンピュータの広範な普及を設定した。一方,コンピュータネットワーク,スーパーコンピュータ,インテリジェント,分散リアルタイムドメインに向かって進んでいる。それにより,分散実時間システムの需要はあらゆる分野で拡大の一途をたどっているので,分散型実時間オペレーティングシステムは自然存在価値を得る。設計の信頼性と正確さを保証するため,本論文では,分散リアルタイムオペレーティングシステムのためのスケジューリングタスクのMDP(Markov決定過程)モデルを構築するための確率的モデル検査を利用する。一方本論文では例としてロボットの分散型実時間オペレーティングシステムをとり,PCTL(確率的計算ツリー論理)におけるいくつかの重要な特性について述べ,ついで,タスクのスケジュール可能性はPRISMによって検証し,解析した。設計者に定量化した結果をフィードバック常に,設計者は,メッセージに基づくいくつかの対応策は,信頼性と妥当性を改善するために取ることができる。Data from the ScienceChina, LCAS. Translated by JST【Powered by NICT】

シソーラス用語： 確率モデル ,  コンピュータ ,  ロボット ,  計算機網 ,  *分散【variance】 ,  信頼性 ,  高速度 ,  スーパコンピュータ ,  デザイナ ,  エノール ,  脂肪族アルコール ,  脂肪族塩素化合物 ,  無機酸エステル
準シソーラス用語： Markov決定過程 ,  *タスクスケジューリング , 【Automatic Indexing@JST】

分類 (2件)： 計算機網  (JC03000K) ,  オペレーティングシステム  (JD03020J)

物質索引 (1件)： ジクロルボス

タイトルに関連する用語 (4件)： PRISM ,  実時間オペレーティングシステム ,  タスクスケジューリング ,  形式的検証