Vol.3 No.3 2010

33/84

研究論文:複雑システムの信頼性を向上させる開発手法(加藤ほか)−209−Synthesiology Vol.3 No.3(2010)参考文献デッドロック:二つ以上の処理単位が互いの処理終了を待ち、結果としてどの処理も先に進めなくなってしまう状態。機能設計:システム仕様として定義される機能を分割・詳細化し、分割・詳細化した機能に対し、システム仕様として定義される性能を配分する作業。物理設計:システムの構成要素を具体化し、機能設計において分割・詳細化した機能・性能を、構成要素に配分する作業。Functional analysis:IEEE 1220 第6章3節に規定される機能設計に該当するプロセス。Synthesis:IEEE 1220 第6章5節に規定される物理設計に該当するプロセス。ブリッジ技術:本論文で明らかにした、アーキテクチャ設計とモデル検査の間をシームレスに繋ぐ技術。トレーサビリティマトリクス:上位仕様と下位仕様の対応関係をまとめた表。有限オートマトン:有限個の状態、遷移、動作の組み合わせからなる振る舞いのモデル。時間オートマトン:有限オートマトンに時間変数を導入した振る舞いのモデル。遷移条件として時間経過をモデル化することができる。SPIN:有限オートマトンベースのモデル検査ツール。PROMELA(Process Meta Language)というC言語に似た言語を用いて、システムの状態遷移をモデル化する。次よりダウンロードが可能。UPPAAL:時間オートマトンに対応したモデル検査ツール。GUI(Graphical User Interface)を用いて、直感的に、システムの状態遷移をモデル化することができる。次よりダウンロードが可能。産業用ロボット:自動制御によるマニピュレーション機能または移動機能を持ち、各種の作業をプログラムによって実行できる、産業に使用可能な機械。サブシステム:システムの一部であるものの、それ自体が局所的な一つのシステムとしての構造を持つもの。COTS:Commercial Off The Shelfの略。ソフトウェア製品やハードウェア製品などの既製品。コンポーネント:サブシステムを構成する要素または部品。ティーチペンダント:産業用ロボットに対する動作のプログラミングや産業用ロボットの緊急停止に用いる装置。コンソール:システムを操作する際に利用する入出力装置。キーボードなどの入力装置、ディスプレイなどの表示装置で構成される。QCD:Quality(開発対象の品質)、Cost(開発コスト)、Delivery(開発期間)の略。International council on systems engineering (INCOSE): INCOSE Systems Engineering Handbook version 3.1, 1.5 of 6, INCOSE, USA (2007).N. G. Leveson: SAFEWARE: System Safety and Computers, 515-553, Addison-Wesley Professional, USA (1995).清水久二: アリアン5の爆発事故とソフトウェア安全性に関する国際規格, 安全工学会安全工学誌, 41 (1), 39-42 (2002).国土交通省: FDPシステムの障害の原因調整の結果, 国土交通省(オンライン), 入手先< http://www.mlit.go.jp/kisha/kisha03/12/120312_.html>(参照2009-09-22).加藤淳, 神武直彦, 春山真一郎, 狼嘉彰: モデル検査を用いて組込みシステムにおけるソフトウェアとハードウェアの協調動作に関する要求仕様の不整合を検出する手法, IPSJ Symposium Series, 2009, 65-70 (2009).加藤淳, 狼嘉彰: FPGAとソフトウェアにおける協調動作の整合性に関する評価手法の提案, 情報処理学会第163回ソフトウェア工学研究会研究報告, 2009 (31), 105-112 (2009).E. M. Clarke, O. Grumberg and D. E. Long: Model checking and abstraction, ACM Transactions on Programming Languages and Systems, 16 (5), 1512-1542 (1994).Institute of Electrical and Electronics Engineers (IEEE): IEEE standard for system and software engineering‐System life cycle processes, IEEE 15288-2008 (2008).American National Standard Institute (ANSI)/Electronic Industries Alliance (EIA): ANSI/EIA Standard for Process for Engineering a System, ANSI/EIA 632-1999 (1999).Institute of Electrical and Electronics Engineers (IEEE): IEEE standard for application and management of the systems engineering process, IEEE 1220-2005 (2005).E. M. Clarke and J. M. Wing: Formal methods: State of the art and future directions, ACM Computing Surveys, 28 (4), 626-643 (1996).International Electrotechnical Commission (IEC): IEC standard for functional safety of electrical/electronic/programmable electronic safety-related systems, IEC 61508-SER Ed. 1.0 (2005).T. DeMarco: Structured Analysis and System Specification, Yourdon Press, USA (1978).有澤誠, 斉藤鉄也: モデルシミュレーション技法, 16-17, 共立出版 (1997).V. K. Rompaey, D. Verkest, I. Bolsens and D. H. Man: CoWare – A design environment for heterogeneous hardware/software systems, Proceedings of the European Design Automation Conference, 252-257 (1996).[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15]用語18:用語19:用語20:用語21:用語22:用語23:用語24:用語25:用語26:用語27:用語28:用語29:用語30:用語31:用語32:用語33:用語34:用語35:時相論理:時間との関連で問題を理解し表現するための規則と表記法の体系。時相演算子、パス限量子、論理演算子を組み合わせ、“常にPが成立する”、“いずれQが成立する”などの性質を表現することができる。時相演算子:時相論理における“G:常に”や、“F:いずれ”などを表現する演算子。パス限量子:時相論理における“A:すべてのパスで”や、“E:あるパス”を表現する演算子。論理演算子:論理演算を表す記号。“NOT:否定”、“AND:論理積”、“OR:論理和”がある。用語36:用語37:用語38:用語39:

※このページを正しく表示するにはFlashPlayer9以上が必要です