文献

J-GLOBAL ID：201702231847654837   整理番号：17A0158320

時間マルチホップネットワークに基づく実時間システムの検証【JST・京大機械翻訳】

Verification of Real-Time Systems with Time Multi-Pushdown Net

著者 (5件)： Qian Junyan (Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology) ,  Gan Pengcheng (Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology) ,  Guo Yunchuan (Institute of Information Engineering, Chinese Academy of Sciences) ,  Zhao Lingzhong (Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology) ,  Gu Tianlong (Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology)
資料名： Jisuanji Xuebao  (Jisuanji Xuebao)
巻： 39  号： 11  ページ： 2253-2269  発行年： 2016年 
JST資料番号： C2531A  ISSN： 0254-4164  CODEN： JIXUDT  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： マルチスレッドネットワーク(MPDN)は,複数のスタックを使用することによって,再帰的プログラムスレッドの間の相互作用を記述するためのダウンシステムモデルである。スレッド間の相互作用に基づく実時間同時再帰プログラムを記述するために,まず第一に,連続時間を記述するクロックをMPDNに導入して,時間的マルチホップネットワーク(TMPDN)を提案して,構文論と操作意味論を与えた。第二に,時間ポイントに基づくクロック等価最適化技術を用いて,等価状態空間を縮減した。次に,静的変換法を用いて,すべての可達域状態パターンを得て,連続時間のTMPDNモデルを離散的MPDNモデルに変換した。これに基づき、ON-THE-FLY技術に基づき、動的転換方法を採用して、桟頂域状態遷移に関心を持ち、さらに変換後の状態空間を削減する。同時に,状態Q_FがTMPDNに到達するとき,Q_F′がMPDNに到達し,モデル変換アルゴリズムを与えることを証明した。最後に,既存のモデル検査ツールを用いて,変換後のMPDN.を検証することができた。Data from the ScienceChina, LCAS. Translated by JST【JST・京大機械翻訳】

シソーラス用語： *スレッド ,  モデル検査 ,  構文論 ,  操作的意味論 ,  アルゴリズム ,  連続時間系 ,  最適化手法 ,  相互作用 ,  クロック
準シソーラス用語： 状態遷移 ,  状態空間 ,  *実時間 ,  *実時間システム ,  *マルチホップネットワーク , 【Automatic Indexing@JST】

著者キーワード (5件)： MPDN ,  TMPDN ,  concurrent recursive programs ,  clock equivalence ,  reachability

分類 (1件)： 人工知能  (JE08000Z)

タイトルに関連する用語 (3件)： マルチホップネットワーク ,  実時間システム ,  検証