TY - JOUR
T1 - モデル変換と振る舞い検証を活用した組み込み制御ソフトウェア設計法 (ディペンダブルコンピューティング 組込み技術とネットワークに関するワークショップETNET2013)
AU - 田村 雅成, null
AU - 兪 明連, null
AU - 横山 孝典, null
AU - YOO, Myungryun
PY - 2013/3/13
Y1 - 2013/3/13
N2 - 組み込み制御ソフトウェア開発の効率向上のため,Simulinkモデルから実装を考慮したUMLモデルを効率的に設計する手法を提案する.一般に,組み込み制御ソフトウェア開発は制御ロジックを作成する制御設計と制御ロジックを元にソフトウェアモデルを作成するソフトウェア設計の2段階で行う.近年の制御設計ではMATLAB/Simulinkを用いて制御ロジックをSimulinkモデルとして設計することが多い.しかし,MATLAB/Simulinkはプリエンプティブなマルチタスク環境でのタスク間のプリエンプションなどについては考慮していない.そのため,制御ロジックをそのままソフトウェアとして実装する場合,プリエンプションによってデータの不整合が発生する恐れがあり,同期や通信の処理を追加する必要がある.我々はこれまでに,制御設計からソフトウェア設計への移行をスムーズに行うため,Simulinkモデルをソフトウェア設計に適した形のUMLモデルに変換するモデル変換ツールを開発してきた.本論文では,生成されたUMLモデルをプリエンプティブなマルチタスク環境で実行した場合に起こりうるデータの不整合を,モデル検査ツールSPINを用いて発見する手法を提案する.そして,モデル変換ツールが生成したUMLモデルから検証用のPROMELAコードを自動生成するツールを開発する.これにより,効率的なソフトウェア設計を可能とする.
AB - 組み込み制御ソフトウェア開発の効率向上のため,Simulinkモデルから実装を考慮したUMLモデルを効率的に設計する手法を提案する.一般に,組み込み制御ソフトウェア開発は制御ロジックを作成する制御設計と制御ロジックを元にソフトウェアモデルを作成するソフトウェア設計の2段階で行う.近年の制御設計ではMATLAB/Simulinkを用いて制御ロジックをSimulinkモデルとして設計することが多い.しかし,MATLAB/Simulinkはプリエンプティブなマルチタスク環境でのタスク間のプリエンプションなどについては考慮していない.そのため,制御ロジックをそのままソフトウェアとして実装する場合,プリエンプションによってデータの不整合が発生する恐れがあり,同期や通信の処理を追加する必要がある.我々はこれまでに,制御設計からソフトウェア設計への移行をスムーズに行うため,Simulinkモデルをソフトウェア設計に適した形のUMLモデルに変換するモデル変換ツールを開発してきた.本論文では,生成されたUMLモデルをプリエンプティブなマルチタスク環境で実行した場合に起こりうるデータの不整合を,モデル検査ツールSPINを用いて発見する手法を提案する.そして,モデル変換ツールが生成したUMLモデルから検証用のPROMELAコードを自動生成するツールを開発する.これにより,効率的なソフトウェア設計を可能とする.
M3 - Misc
SN - 0913-5685
VL - 112
SP - 181
EP - 186
JO - 電子情報通信学会技術研究報告 : 信学技報
JF - 電子情報通信学会技術研究報告 : 信学技報
IS - 482
ER -