抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
本研究は,UPPAALを用いて記述した時間オートマトンによる振舞い仕様からLEGO Mindstorm EV3システムを制御するC言語プログラムを合成する手法を提案する。UPPAALは複数の時間オートマトンがネットワークで同期しながら計算が進行する振舞いを記述し,制限されたCTLによって記述された性質に対するモデル検査を行うツールである。LEGO Mindstorm EV3の振舞いをモジュール毎に時間オートマトンで時間依存の振舞いの概略を記述し,さらに詳細を記述したC言語を合成することで全体の制御プログラムを合成する。詳細のC言語プログラムが局所的に性質を満していれば,全体の仕様を満たす制御プログラムが合成可能であるため,特に時間制約による組合せに起因する誤りを有効に発見することができる。ブロックの色による仕分け装置に本手法を適用してプログラムの合成手法を示す。(著者抄録)