@techreport{oai:ipsj.ixsq.nii.ac.jp:00233443,
 author = {近藤, 大起 and 磯部, 祥尚 and 枝廣, 正人},
 issue = {12},
 month = {Mar},
 note = {制御システムでは大規模・複雑化が進み，逐次で処理をするシングルコアよりも，並列化によって高速処理を可能にするマルチ・メニーコアによる並列制御が注目され，開発されている．しかし，並列制御では再現性のない実行順序逆転やデッドロックが発生するなど，逐次制御にはない特有の問題がある．さらに，サンプリング周期の異なるデータや実行時間の異なる処理の混在を可能にするマルチレート制御では，実行順序の制御はさらに複雑になるため，マルチレート制御の逐次コードを並列化するには細心の注意が必要である．我々は制御システムの逐次的なモデルから，その観測的な振舞いを変えずに並列制御の実行コードを自動生成するモデルベース並列化システム MBP を開発している．本論文では，MBP のシングルレートの制御モデルの並列化アルゴリズムをベースに開発したマルチレート制御モデルの並列化アルゴリズム MR MBP Algo とその開発方法について提案する．生成する並列制御モデルを可読性の高い構造図とステートマシン図によって設計し，その設計を形式記述言語 CSP によって厳密に記述して，その形式記述をモデル検査器 FDR によって網羅的に検証しており，再現性のない不具合の原因となるアルゴリズムの設計ミスを実装前に発見し，設計を修正することが可能である．},
 title = {マルチレート制御モデル並列化アルゴリズムの設計と形式検証},
 year = {2024}
}