文献
J-GLOBAL ID:202202287766408714
整理番号:22A0884622
モデルベース並列化アルゴリズムの定理証明器による形式検証
-
出版者サイト
{{ this.onShowPLink() }}
複写サービスで全文入手
{{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=22A0884622©=1") }}
-
高度な検索・分析はJDreamⅢで
{{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=22A0884622&from=J-GLOBAL&jstjournalNo=U0451A") }}
著者 (3件):
,
,
資料名:
巻:
2022
号:
ARC-248
ページ:
Vol.2022-ARC-248,No.54,1-10 (WEB ONLY)
発行年:
2022年03月03日
JST資料番号:
U0451A
資料種別:
会議録 (C)
記事区分:
原著論文
発行国:
日本 (JPN)
言語:
日本語 (JA)
抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
制御システムの大規模・複雑化にともない,並列化によって高速処理を可能にするメニーコアによる並列制御が注目されている.しかし,並列動作には実行順序逆転やデッドロックなど,逐次動作にはない特有の問題があり,人手による並列化は容易ではない.そこで,我々は制御システムの逐次的なモデルから,それと等価な並列制御の実行コードを自動生成するモデルベース並列化システムMBPを開発している.本論文では,MBPの並列化アルゴリズムを形式仕様記述言語CSPで厳密に記述し,定理証明器Isabelleを用いて,実行順序逆転やデッドロックが起こらないことを証明したことを報告する.(著者抄録)
シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
,
,
,
,
,
,
,
準シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
分類 (1件):
分類
JSTが定めた文献の分類名称とコードです
情報工学基礎理論一般
引用文献 (10件):
-
MathWorks Makers of MATLAB and Simulink. 入手先 <http://www.mathworks.co.jp.>
-
鍾兆前, 枝廣正人: モデルベース開発におけるマルチ・メニーコア向け自動並列化, ETNET2017, 電子情報通信学会技術研究報告, Vol. 2017-EMB-44, No. 47, pp.273-278, 2017.
-
山口滉平, 竹松慎弥, 池田良裕, 李瑞徳, 鍾兆前, 近藤真己, 枝廣正人: Simulink モデルからのブロックレベル並列化, 情報処理学会 組込みシステムシンポジウム(ESS), pp.123-124, 2015.
-
山本尚平, 鈴木悠太, 峰田憲一, 森裕司, 枝廣正人: モデルベース並列化におけるCSPモデルを利用した形式検証の適用, ETNET2017, 電子情報通信学会技術研究報告, Vol.2017-EMB-44, No.6, pp.33-38, 2017.
-
于文博, 磯部祥尚, 枝廣正人: 共有メモリ付階層型制御モデルの並列化アルゴリズムのCSPによる形式化と FDR による検証, ETNET2020, 電子情報通信学会技術研究報告, Vol. 2020-EMB-44, No. 40, pp.1-12, 2020.
もっと見る
タイトルに関連する用語 (5件):
タイトルに関連する用語
J-GLOBALで独自に切り出した文献タイトルの用語をもとにしたキーワードです
,
,
,
,
前のページに戻る