文献
J-GLOBAL ID:201402207768725603   整理番号:14A1500431

UPPAALを用いたLEGO mindstorms EV3制御プログラムの合成

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

準シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。

分類 (1件):
分類
JSTが定めた文献の分類名称とコードです
システムプログラミング一般 
引用文献 (5件):
  • LEGO.com Education Home, http://education.lego.com/.
  • David L Dill Rajeev Alur. A theory of timed automata. Theoretical computer science 126. 1994. pp.182-235.
  • 中田明夫. 時間オートマトンによる実時間システムの形式的検証. 計測と制御, 第48巻, 第11号. 計測自動制御学会, 11, 2009. pp.1-7.
  • UPPALL. http://www.uppaal.org/.
  • Eunkyoung Jee, Shaohui Wang, Jeong Ki Kim, Jaewoo Lee, Oleg Sokolsky, Insup Lee. A Safety-Assured Development Approach for Real-Time Software. RTCSA. August, 2010. pp.133-142.
タイトルに関連する用語 (2件):
タイトルに関連する用語
J-GLOBALで独自に切り出した文献タイトルの用語をもとにしたキーワードです

前のページに戻る