文献

J-GLOBAL ID：202202287766408714   整理番号：22A0884622

モデルベース並列化アルゴリズムの定理証明器による形式検証

著者 (3件)： 岩田駿 (名古屋大 大学院情報学研究科) ,  磯部祥尚 (産業技術総合研) ,  枝廣正人 (名古屋大 大学院情報学研究科)
資料名： 情報処理学会研究報告(Web)  (IPSJ Technical Report (Web))
巻： 2022  号： ARC-248  ページ： Vol.2022-ARC-248,No.54,1-10 (WEB ONLY)  発行年： 2022年03月03日 
JST資料番号： U0451A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 制御システムの大規模・複雑化にともない,並列化によって高速処理を可能にするメニーコアによる並列制御が注目されている.しかし,並列動作には実行順序逆転やデッドロックなど,逐次動作にはない特有の問題があり,人手による並列化は容易ではない.そこで,我々は制御システムの逐次的なモデルから,それと等価な並列制御の実行コードを自動生成するモデルベース並列化システムMBPを開発している.本論文では,MBPの並列化アルゴリズムを形式仕様記述言語CSPで厳密に記述し,定理証明器Isabelleを用いて,実行順序逆転やデッドロックが起こらないことを証明したことを報告する.(著者抄録)

シソーラス用語： 解析 ,  並列化 ,  *並列処理 ,  アルゴリズム ,  デッドロック ,  *制御プログラム ,  *形式的仕様記述言語 ,  定理証明
準シソーラス用語： モデルベース解析

分類 (1件)： 情報工学基礎理論一般  (JB01000T)

引用文献 (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件)： モデルベース ,  並列化 ,  アルゴリズム ,  定理証明 ,  形式検証