2026-04-20T19:36:06Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00217274 2025-01-19T15:33:31Z 1164:2822:10894:10895

モデルベース並列化アルゴリズムの定理証明器による形式検証 岩田, 駿 磯部, 祥尚 枝廣, 正人 並列処理・モデルベース・設計手法 制御システムの大規模・複雑化にともない，並列化によって高速処理を可能にするメニーコアによる並列制御が注目されている．しかし，並列動作には実行順序逆転やデッドロックなど，逐次動作にはない特有の問題があり，人手による並列化は容易ではない．そこで，我々は制御システムの逐次的なモデルから，それと等価な並列制御の実行コードを自動生成するモデルベース並列化システム MBP を開発している．本論文では，MBP の並列化アルゴリズムを形式仕様記述言語 CSP で厳密に記述し，定理証明器 Isabelle を用いて，実行順序逆転やデッドロックが起こらないことを証明したことを報告する． technical report 情報処理学会 2022-03-03 application/pdf 研究報告組込みシステム（EMB） 54 2022-EMB-59 1 10 2188-868X AA12149313 https://ipsj.ixsq.nii.ac.jp/record/217274/files/IPSJ-EMB22059054.pdf jpn