文献

J-GLOBAL ID：201502210174136224   整理番号：15A1113636

CoqにおけるμC/OS IIIタスクスケジューラの検証【Powered by NICT】

Verification of μC / OS-III Task Scheduler in Coq

著者 (2件)： Luo Ercong (Coll. of Computer Sci. and Technol.,Univ. of Sci. and Technol. of China, Hefei) ,  Guo Yu (Coll. of Computer Sci. and Technol.,Univ. of Sci. and Technol. of China, Hefei)
資料名： Jisuanji Gongcheng  (Jisuanji Gongcheng)
巻： 41  号： 3  ページ： 53-58  発行年： 2015年 
JST資料番号： C2532A  ISSN： 1000-3428  CODEN： JISGEV  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： に埋め込まれた広く使用されているμC/OS IIIカーネルにおけるタスクスケジューラを研究した。スケジューラからコア部分を選択した後,スケジューラの特性を特定する。分離論理とSCAPに基づいて,機械モデル,操作的意味論,アサーション言語,推論ルールを含む検証フレームワークを構築した。枠組みでは,システムデータ構造と性質を特定する主張を定義し,システムコードは約モジュールと推論できた。μC/OS IIIにおけるタスクスケジューラの特性が形式的に証明され,研究によって提供された全証明した機械検査可能。Data from the ScienceChina, LCAS. Translated by JST【Powered by NICT】

シソーラス用語： 力学モデル ,  データ構造 ,  *操作的意味論 ,  モジュール ,  言語 ,  穀粒
準シソーラス用語： アサーション , 【Automatic Indexing@JST】

分類 (1件)： オペレーティングシステム  (JD03020J)

タイトルに関連する用語 (4件)： Os ,  タスク ,  スケジューラ ,  検証