WEKO3
アイテム
モデルベース並列化アルゴリズムの定理証明器による形式検証
https://ipsj.ixsq.nii.ac.jp/records/217208
https://ipsj.ixsq.nii.ac.jp/records/2172080884a4ca-fdbd-46f2-b17e-b8c17fe18729
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SLDM22198054.pdf (1.5 MB)
|
Copyright (c) 2022 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2022-03-03 | |||||||||||
| タイトル | ||||||||||||
| タイトル | モデルベース並列化アルゴリズムの定理証明器による形式検証 | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | 並列処理・モデルベース・設計手法 | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||
| 資源タイプ | technical report | |||||||||||
| 著者所属 | ||||||||||||
| 名古屋大学大学院情報学研究科 | ||||||||||||
| 著者所属 | ||||||||||||
| 産業技術総合研究所 | ||||||||||||
| 著者所属 | ||||||||||||
| 名古屋大学大学院情報学研究科 | ||||||||||||
| 著者名 |
岩田, 駿
× 岩田, 駿
× 磯部, 祥尚
× 枝廣, 正人
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 制御システムの大規模・複雑化にともない，並列化によって高速処理を可能にするメニーコアによる並列制御が注目されている．しかし，並列動作には実行順序逆転やデッドロックなど，逐次動作にはない特有の問題があり，人手による並列化は容易ではない．そこで，我々は制御システムの逐次的なモデルから，それと等価な並列制御の実行コードを自動生成するモデルベース並列化システム MBP を開発している．本論文では，MBP の並列化アルゴリズムを形式仕様記述言語 CSP で厳密に記述し，定理証明器 Isabelle を用いて，実行順序逆転やデッドロックが起こらないことを証明したことを報告する． | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AA11451459 | |||||||||||
| 書誌情報 |
研究報告システムとLSIの設計技術（SLDM） 巻 2022-SLDM-198, 号 54, p. 1-10, 発行日 2022-03-03 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-8639 | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
