計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

構成要素の連携動作に着目した産業用ロボットの開発：
IEEE 1220 におけるアーキテクチャ設計プロセスおよび
UPPAAL によるモデル検査を融合した開発手法の提案
加藤淳*，浦郷正隆*，狼嘉彰*
Development of Industrial Robot focusing on Cooperating Behavior among Robot Elements:
A Methodology for combining Architectural Design Process in IEEE 1220 andModel Checking by UPPAAL
Atsushi Katoh*, Masataka Urago* and Yoshiaki Ohkami*
On developing industrial robots, there are some cases that flaws are incorporated in designing cooperating behavior
among elements in an industrial robot, due to complexity of the industrial robot. The cooperating behavior among elementsin the industrial robot is generally verified in a system test which is conducted by combining element products on a final
development phase. There are impacts to the whole development of the industrial robot when inconsistency of cooperating
behavior among the elements is detected in the system test. Therefore, the cooperating behavior among the elements in theindustrial robot must be surely developed on an early phase in the development of the industrial robot. This paper proposes amethodology for decomposing a system specification for an industrial robot into element specifications and interface
specifications for elements. Consistency of cooperating behavior among their specifications is also verified. The proposed
methodology is applied on an system design phase which is an early phase in development of the industrial robot. It is
composed of architectural design method in IEEE 1220 and model checking by UPPAAL. It is adopted to a project fordeveloping the industrial robot. As a result of adopting the methodology, it is demonstrated that the methodology is effective
for developing the industrial robot from the point of view of QCD.
Key Words : industrial robot, cooperating behavior, architectural design process, model checking

複雑化が進んでいる．それに伴い産業用ロボットにおける信

1.

はじめに

頼性の確保が課題になっている．産業用ロボットをシステム

産業用ロボットとは自動制御によるマニピュレーション機
能または移動機能を持ち，各種の作業をプログラムによって実行できる機械である1）．日本は世界に名立たるロボット大国である．世界における産業用ロボットの総稼動台数のうち
約 35%が日本で使用されている2）．また，日本国内における産業用ロボットの生産額は，2006 年には 7,300 億円に達している3）．産業用ロボットは日本におけるモノづくりの代名
詞である自動車産業や電子部品産業などの製造業を支えている．
近年，産業用知能ロボット4）の登場など産業用ロボットの*慶應義塾大学大学院
システムデザイン・マネジメント研究科
神奈川県横浜市港北区日吉 4-1-1(E-mail: katoh.atsushi@z7.keio.jp)*Keio University Graduate School of System Design andManagement(Received June 28, 2010)

として捉えた場合，産業用ロボットはロボットシステムやセンシングシステムなどのシステムが産業用ロボットを構成するサブシステムとして高次に結びついた複雑システムである．
複雑システムではシステムの機能を実現するために，システ
ムを構成する要素の処理がインタフェースを介し，他構成要素の処理と密に連携する．本論文ではこれを構成要素による連携動作と定義する．また，本論文ではシステムの仕様に対してシステムの構成要素による連携動作が正しく行われることを連携動作が整合すると定義する．産業用ロボットではロボットサブシステムやセンシングサブシステムなどの構成要
素による連携動作が整合していることが重要である．しかし，産業用ロボットの開発においては，その複雑性のために構成要素による連携動作の設計に誤りが生じる場合がある．通常，
システムの構成要素による連携動作は，システム開発の終盤に実施される構成要素の実プロダクトを組み合わせたシステ
ム試験で確認される．システム試験において連携動作の不整

TRIA 005/11/1005 © 2010 SICE

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

合を検出した場合，システム開発の上流工程に立ち戻り連携

定形な剛体を運搬する産業用ロボットを開発した事例を具体

動作を再設計する必要がある．その際，開発期間の長期化お的に述べる．5 章において，開発事例を基に産業用ロボット

よび改修によるコスト増を招く．また，システム開発の終盤

開発における提案手法の有効性および課題を考察する．6 章という設計自由度が小さい中での連携動作の設計変更により，

において，本研究の関連研究を述べる．7 章において，本論

システムの信頼性が低下する可能性がある．産業用ロボット

文をまとめる．

の開発においては，市場競争力の観点から開発期間の長期化

2.

およびコスト増，信頼性の低下を避けなければならない．
本論文では産業用ロボット開発の上流工程であるシステム

提案手法を実現する技術

提案する開発手法はつぎに示す 2 つの機能を有する．

設計段階において，産業用ロボットのシステム仕様を連携動a) 産業用ロボットのシステム仕様を産業用ロボットに作が整合している産業用ロボットにおける構成要素の仕様おおける構成要素の仕様および構成要素間のインタフ

よび構成要素間のインタフェース仕様に分解する開発手法を

ェース仕様に分解する機能提案する．われわれは文献5）においてシステムエンジニアb) 構成要素の仕様および構成要素間のインタフェース

リングにおけるアーキテクチャ設計手法および形式手法の 1仕様における連携動作が整合していることを検証すつであるモデル検査の構成方法を示した．本論文では文献

る機能5）に示す構成方法に則って実現される産業用ロボットに関機能 a) を実現するにあたり，IEEE 1220 におけるアーキテ

する開発手法の実例および産業適用の具体例を示す．産業用

クチャ設計プロセスを適用する．また，機能 b) を実現する

ロボット開発の上流工程において，構成要素による連携動作にあたり，UPPAAL によるモデル検査を適用する．
つぎに，IEEE 1220 におけるアーキテクチャ設計プロセスを確実に作り込むことにより産業用ロボットにおける信頼性および UPPAAL によるモデル検査を述べる．
2.1. IEEE 1220 におけるアーキテクチャ設計プロセスの向上を図る開発手法は提案されていない．産業用ロボットの構成要素による連携動作を確実に作り込む手順を具体的に示すことで産業界における産業用ロボットの開発に貢献する．

グ 標準に定められている．システムエンジニアリングとは提案手法を実現するにあたり，IEEE 1220 におけるアーキテ
クチャ設計プロセス

6）

およびモデル検査ツール UPPAAL

アーキテクチャ設計プロセスは，システムエンジニアリン
9）与えられた費用および期間内で必要な品質を満たすシステム

7）を実現する技術体系である．アーキテクチャ設計を含むシス8）によるモデル検査 を適用する．アーキテクチャ設計とはシテムエンジニアリングは，主に軍事，航空・宇宙分野で研究

ステムの構成要素に対しシステムに要求される機能・性能をが始まり，システム開発の Best Practice を蓄積・反映しなが配分し，構成要素の仕様および構成要素間のインタフェース

ら標準化されている．Fig. 1 にアーキテクチャ設計プロセス

仕様を明確化する技術である．IEEE 1220 に規定されるプロを示す．アーキテクチャ設計は機能設計および物理設計で構セスに従いアーキテクチャ設計を実施する．それにより，産成される．機能設計のインプットはシステム仕様である．機

業用ロボットのシステム仕様を構成要素の仕様および構成要

能設計とはシステム仕様に定義される機能を分割・詳細化し，素間のインタフェース仕様に効率的かつ確実に分解すること

分割・詳細化した機能に対しシステム仕様に定義される性能ができる．モデル検査とはシステムの状態遷移を表すモデルを配分する作業である．機能設計のアウトプットは分割・詳に対して，与えられた性質が成り立つか否かを計算機により細化した機能および性能である．それらは物理設計のインプ

網羅的に検証する技術である．アーキテクチャ設計により導ットとなる．物理設計とはシステムを構成する要素を具体化出された構成要素の仕様および構成要素間のインタフェース

し，機能設計において分割・詳細化した機能および性能を構仕様において，構成要素の連携動作に関する部分に着目し成要素に配分する作業である．物理設計のアウトプットはシ

UPPAAL によるモデル検査を適用する．モデル検査によっ

ステムにおける構成要素の仕様および構成要素間のインタフて連携動作が満たすべき性質が成り立つかどうかをしらみつ

Element
Specifications

ぶしに確認する．それにより，複雑な状態で発生する連携動
SystemSpecification

作の不整合を検出することができる．連携動作が整合していIn1る仕様を基に各構成要素の開発を行うことにより，産業用ロArchitectural
Architectural
DesignDesignOut1
Out2

ボットにおける信頼性の向上が期待できる．

Interface
Specification
for Elements

本論文の構成はつぎの通りである．2 章において，提案手法を実現する IEEE 1220 におけるアーキテクチャ設計プロセ

In1
In1

スおよび UPPAAL によるモデル検査を述べる．3 章におい

Functional
Functional
DesignDesignPhysicalPhysicalDesignDesign

Out1
Out1
Out2
Out2

て，提案手法を述べる．4 章において，提案手法を適用し不Fig. 1 Process of Architectural Design38計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)章 3 節 Functional analysis に定められている．Fig.3 に IEEE

ェース仕様である．

1220 に規定される物理設計のプロセスを示す．IEEE 1220 にアーキテクチャ設計に関する詳細なプロセスは，システムエンジニアリング標準である IEEE 1220 に定められている．

おける物理設計のプロセスは，IEEE 1220 第 6 章 5 節

Fig.2 に IEEE 1220 に規定される機能設計のプロセスを示す．

Synthesis に定められている．Fig.2 および Fig.3 において番号IEEE 1220 における機能設計のプロセスは，IEEE 1220 第 6が付与されたボックスは，実施すべきタスクを表す．IEEE
1220 にはそれぞれのタスクで実施すべき作業内容が定めら
れている．

6.3

IEEE 1220 は，さまざまな産業ドメインにおいて適用されFunctional
Functional analysis
analysis

成果を上げている10）．そのため，IEEE 1220 の適用には一定の有効性が保証される．一例を挙げるとアメリカ航空宇宙局

6.3.1
Functional
context analysis（NASA）では IEEE 1220 の有効性を認め，宇宙機や宇宙機
6.3.1.2

6.3.1.1

DefineDefinefunctional
functional
interfaceinterface

Analyze
Analyzefunctional
functional
behaviors
behaviors
6.3.2
Functional
decomposition

6.3.1.3を管制する地上システムなどを開発する際の要求に IEEE

Allocate
Allocate
performance
performancerequirements
requirements

1220 のエッセンスを組み込んでいる11）．Fig.2 および Fig.3の番号に従い IEEE 1220 に定められる作業を実施することで，6.3.2.1
DefineDefinesubfunctions
subfunctions

6.3.2.4

6.3.2.3

6.3.2.5の仕様および構成要素間のインタフェース仕様に分解することができる．
2.2. UPPAAL によるモデル検査

6.3.2.6

DefineDefine functional
functional
FailureFailure modes
modes
And
And effects
effects

DefineDefine data
data andandControl
Control flows
flows

DefineDefine functional
functional
timelines
timelines

産業用ロボットのシステム仕様を効率的かつ確実に構成要素

6.3.2.2
DefineDefinesubfunctions
subfunctions
statesstates andand modes
modes

モデル検査とは形式手法12）のひとつに位置付けられる検DefineDefine safety
safetymonitoring
monitoring
functionsfunctions

証技術である．モデル検査は 1980 年代初頭より研究が開始され，近年，ソフトウェア開発において普及が進んでいる．

6.3.3

Fig. 4 にモデル検査の概要を示す．モデル検査のプロセスは

Establish
Establish functional
functional architecturearchitecture

モデルの作成，検査式の作成，モデル検証の実施，検証結果の分析という 4 つの作業に大別される．まず，適用するモデ
ル検査ツールの表現形式に従って，検査対象となるシステム

Fig. 2 Process of Functional Design in IEEE 12206）の仕様などを基に検査対象の状態遷移をモデル化する．つぎに，適用するモデル検査ツールの表現形式に従って，検査対象が満たすべき性質を表す検査式を作成する．そして，計算

6.5
Synthesis
Synthesis

機上のモデル検査ツールに対して，モデルと検査式を入力し

6.5.1

6.5.2

モデル検証を実施する．モデル検証ではモデルが実現しうるGroup
Group andand allocate
allocatefunctionsfunctions

Identify
Identify design
designsolutionsolution alternatives
alternatives

すべての状態遷移において，モデルが検査式を満足するか否

6.5.3

6.5.4

AssessAssess safety
safety andandenvironmental
environmental hazards
hazards

AssessAssess life
life cycle
cycle quality
qualityfactors
factors

6.5.6
DefineDefine design
design andand
Performance
Performance
characteristics
characteristics
6.5.8

6.5.11

Specification
for Target System

DefineDefine physicalphysicalInterfaces
Interfaces

In1

6.5.10Identify
Identify off-the-shelf
off-the-shelfavailability
availability

6.5.12Develop
Develop models
models andandFabricate
Fabricate prototypes
prototypesに，モデルと検査式との適合結果を分析する．モデルに対しAssessAssess technology
technology
requirements
requirements

6.5.7

6.5.9

Identify
Identify standardization
standardization
opportunities
opportunities

かを網羅的に検証する．その後，モデル検証の出力結果を基

6.5.5

AssessAssess testability
testability
needs
needs

AssessAssess design
designCapacity
Capacity toto evolve
evolveorProperties
satisfied.

Counterexample
Counterexample

In1
In1

Finalize
Finalize design
designInitiate
Initiate evolutionary
evolutionary
development
development

Results ofModel Checking

Out1

Properties
NOT satisfied.

6.5.146.5.156.5.16Model
Model
Checking
Checking

Properties
for Target System

Identify
Identify makemake oror buybuy
alternatives
alternatives

6.5.13

AssessAssess failure
failure modes,
modes,
effects,
effects, andand criticality
criticality

In2

Modeling
Modeling
State
State Transitions
Transitions
inTargetin Target System
SystemAnalyzing
Analyzing
Model
Model Verification
Verification
Results
Results

Model
Model
Verification
Verification

6.5.17
Produce
Produce integrated
integrated data
data
packagepackage

In2
In2

Formalizing
Formalizing
Properties
Properties
inin Target
Target System
System

6.5.18“P” should be satisfied
in all reachable states.

Establish
Establish design
designarchitecturearchitecture

AG P
EF Q

PP

PP
PP

PP

PP
PP

PP

“Q” should be satisfied
in some reachable states.

Fig. 3 Process of Physical Design in IEEE 12206）

PP
PP

Fig. 4 Overview of Model Checking

39

Q
Q

Out1
Out1

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)て検査式が適合しない場合，検査式が成り立たない条件に至る状態遷移のパスで），論理演算子（OR，AND，NOT）をるまでのモデルの状態遷移が反例として出力される．反例を組み合わせた時相論理15）で表現される．UPPAAL における分析しモデルに誤りが無い場合，モデルの基になった検査対

反 例 の 分 析 に も GUI を 用 い る こ と が で き る ． Fig. 6 に象の仕様に誤りがあることを意味する．

UPPAAL における反例の出力例を示す．Fig. 6 上部に示すウ

モデル検査における計算モデルの代表的な種類として，有限オートマトン13）および時間オートマトン14）が挙げられる．
有限オートマトンとは有限個の状態，状態遷移，状態遷移時
における動作の組み合わせからなる振る舞いのモデルである．
時間オートマトンとは有限オートマトンに時間変数を導入しィンドウには，検査式が成り立たない状態に至るまでの状態遷移のパスが出力される．Fig. 6 上部のウィンドウにおいて状態遷移のパスを遡る場合，それに対応する状態遷移が Fig.
6 下部に示す状態遷移モデルに表示される．UPPAAL の詳細については文献16）にまとめられている．

たモデルである．産業用ロボットは決められた時間内に処理

産業用ロボットの構成要素において連携動作の状態遷移にを終了する必要があるなどの時間制約を有する場合が多い．

デッドロックなどの不整合が存在する場合，産業用ロボット

したがって，提案手法では時間的な制約を評価することが可
能な時間オートマトンに対応したモデル検査ツールであるの安全性に対して致命的な影響を与える可能性がある．

UPPAAL を適用する．

UPPAAL によるモデル検査を適用して連携動作に関する状

UPPAAL におけるモデルの作成は，GUI（Graphical User

態遷移を網羅的に検証する．それにより，連携動作の不整合Interface）を用いて直感的に行うことができる．Fig. 5 にを検出し連携動作における状態遷移に起因する危険性を排除

UPPAAL モデルの例を示す．Fig. 5 において◎は初期状態，

することができる．

○はその他の状態を表す．矢印は状態遷移，矢印に付記され3.

る条件式（"=="）は遷移条件を表す．矢印に付記される代入

提案手法

式 （ "=" ） は モ デ ル 上 の 変 数 に 対 す る 値 の 設 定 を 表 す ．

本章では，IEEE 1220 におけるアーキテクチャ設計プロセ

UPPAAL における検査式は時相演算子（G：常に，F：いずスおよび UPPAAL によるモデル検査を融合した開発手法をれ），パス限量子（A：すべての状態遷移のパスで，E：あ述べる．Fig. 7 に提案手法を示す．提案手法のインプットは
産業用ロボットのシステム仕様である．提案手法のアウトプ
ットは連携動作が整合している産業用ロボットにおける構成要素の仕様および構成要素間のインタフェース仕様である．
Fig. 1 で表される IEEE 1220 におけるアーキテクチャ設計は，Fig. 7 左側の網掛けボックスに該当する．Fig. 4 で表される
UPPAAL によるモデル検査は，Fig. 7 右側の網掛けボックスに該当する．IEEE 1220 におけるアーキテクチャ設計のアウ
トプットおよび UPPAAL によるモデル検査のインプットを
シームレスに接続するために，アーキテクチャ設計およびモデル検査の間につぎに示す作業を設定する．

Fig. 5 Sample Model on UPPAAL

 構成要素の連携動作に関する仕様の抽出（Fig. 7 中央
上部の白抜きボックス） 構成要素の連携動作が満たすべき性質の抽出（Fig. 7
Consistency of
Cooperating Behavior
Verified
Element
Specifications
SystemSpecification

Architectural
Architectural
DesignDesignElement
Specifications
Interface
Specifications
for Elements

In1
In1
Traceability
MatrixFig. 6 Sample of Counterexample

In1

Proposed
Proposed
Methodology
Methodology

Extraction
Extraction ofofSpecification
Specification forfor
Cooperating
Cooperating
Behavior
Behavior
among
among Elements
Elements
Identification
Identification ofof
Properties
Properties forfor
Cooperating
Cooperating
Behavior
Behavior
among
among Elements
Elements

Out1
Out2

Interface
Specification
for Elements

Properties satisfied
Out1
Out1
Model
Model
Checking
Checking

Properties NOT satisfied

Fig. 7 Process of Proposed Methodology
40

Out2
Out2

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

不定形剛体運搬ロボットシステム仕様 6.1.8.2.a「Function of

中央下部の白抜きボックス）
つぎより提案手法のプロセスに従い，その詳細を述べる．

Grasping Objects（剛体把持機能）」を基に，ロボット制御サ3.1. アーキテクチャ設計

ブシステム仕様 3.1.1.1「Function of Controlling Robot Arm and

産業用ロボットのシステム仕様をインプットとして，Robot Hand for Grasping Objects（剛体把持におけるロボットIEEE 1220 に定められるプロセスに従いアーキテクチャ設計

アームおよびロボットハンド制御機能）」および計測制御サを実施する．アーキテクチャ設計のアウトプットは，産業用ブシステム仕様 6.1.2.1「Function of Sensing Objects（剛体測ロボットにおける構成要素の仕様および構成要素間のインタ定機能）」を連携動作する仕様として抽出する．Fig. 9 におフェース仕様である．また，アーキテクチャ設計の過程において各サブシステムの仕様における連携動作に関する箇所は，

いて，システム仕様および構成要素の仕様におけるトレーサ

ロボット制御サブシステム仕様および形状測定サブシステム

ビリティマトリクスを作成する．Fig. 8 に 4 章で述べる不定仕様における縞模様部分である．また，構成要素間のインタ

形剛体運搬ロボットシステムの開発におけるトレーサビリテ

フェース仕様から連携動作に関する仕様を抽出する際，構成ィマトリクスを例示する．不定形剛体運搬ロボットシステム

要素の連携動作の仕様における他構成要素とのインタラクシの仕様がシステム仕様に対応する．ロボット制御サブシステ

ョン情報を用いる．ここでのインタラクションとは，構成要

ムおよび形状測定サブシステムの仕様が構成要素の仕様に対素間におけるメッセージ送受信などを意味する．構成要素間応する．トレーサビリティマトリクスには仕様に付与した項のインタフェース仕様において，抽出したインタラクション

番単位で，システム仕様とそれをブレークダウンした構成要情報に対応する仕様が連携動作に関するインタフェース仕様

素の仕様との対応関係をまとめる．

である．Fig. 9 においてサブシステム間のインタフェース仕

3.2. 構成要素の連携動作に関する仕様の抽出様における連携動作に関する箇所は，中央のメッセージ部分

アーキテクチャ設計のアウトプットである産業用ロボット

である．

における構成要素の仕様，構成要素間のインタフェース仕様，

3.3. 構成要素の連携動作が満たすべき性質の抽出

システム仕様および構成要素の仕様におけるトレーサビリテ

システム仕様，システム仕様および構成要素の仕様におけィマトリクスをインプットとして，連携動作に関する仕様をるトレーサビリティマトリクスをインプットとして，産業用抽出する．本作業のアウトプットは構成要素の仕様および構ロボットの構成要素における連携動作が満たすべき性質を抽成要素間のインタフェース仕様から抽出した連携動作に関す出する．本作業のアウトプットは構成要素による連携動作がる仕様である．Fig. 9 に 4 章で述べる不定形剛体運搬ロボッ

満たすべき性質である．構成要素による連携動作は，連携動トシステムにおける連携動作に関する仕様を例示する．ロボ

作することにより実現するシステムの仕様を満足する必要がット制御サブシステムおよび形状測定サブシステムの仕様がある．連携動作が満たすべき性質は，連携動作の仕様に対応

構成要素の仕様に対応する．サブシステム間のインタフェー

するシステム仕様中に存在する．したがって，トレーサビリ

ス仕様が構成要素間のインタフェース仕様に対応する．構成

ティマトリクスを用いて連携動作の仕様からそれに対応する要素の仕様から連携動作に関する仕様を抽出する際，システシステム仕様を導出し，導出したシステム仕様から連携動作

ム仕様および構成要素の仕様におけるトレーサビリティマトが満たすべき性質を抽出する．Fig. 8 の場合，ロボット制御

リクスを用いる．トレーサビリティマトリクスを用いて，シ

サブシステム仕様 3.1.1.1「Function of Controlling Robot Arm

ステムの仕様が複数の構成要素に対応付けられる仕様を構成

and Robot Hand for Grasping Objects（剛体把持におけるロボ要素による連携動作の仕様として抽出する．Fig. 8 の場合，

ットアームおよびロボットハンド制御機能）」および計測制

Robot System Specification
for Carrying Indeterminate-form and Rigid Objects

Sub-System onControlling Robot

6.1.8.2.a Function of Grasping Objects
6.1.8.2.b Function of Carrying Objects
Sub-System Specification
for Controlling Robot

Sub-System Specificationfor Sensing Shape

3.1.1.1 Function of Controlling Robot Arm and Robot Hand
for Grasping Objects
3.1.2.1 Function of Controlling Robot Arm and Robot Hand
for Carrying Objects

6.1.2.1 Function of Sensing Objects

Traceability Matrix
on Robot System Specification－
Sub-System Specification for Controlling Robot
Robot System Specification

Sub-System Specification
for Controlling Robot

6.1.8.2.a
Function of Grasping Objects

3.1.1.1
Function of Controlling Robot
Arm and Robot Hand for
Grasping Objects

6.1.8.2.b
Function of Carrying Objects

3.1.2.1
Function of Controlling Robot
Arm and Robot Hand for
Carrying Objects

Sub-System Specification
for Controlling Robot

Sub-System on
Sensing Shape

Interface
Specificationfor Sub-Systems

Sub-System Specificationfor Sensing Shape

Traceability Matrix
on Robot System Specification－
Sub-System Specification for Sensing Shape
Robot System Specification

Sub-System Specificationfor Sensing Shape

6.1.8.2.a
Function of Grasping Objects

6.1.2.1
Function of Sensing Objects

6.1.8.2.b
Function of Carrying Objects

N/A

Message

Processing

Specification concerned withcooperating behavior

Fig. 9 Specifications concerned with Cooperating Behavior

Fig. 8 Traceability Matrix

41計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

御サブシステム仕様 6.1.2.1「Function of Sensing Objects（剛テム仕様書の策定においては仕様の 1 つ 1 つに対して項番を体測定機能）」による連携動作が満たすべき性質は，不定形付与した．これはアーキテクチャ設計の過程で作成するトレ

剛体運搬ロボットシステム仕様 6.1.8.2.a「Function ofーサビリティマトリクスにおいて，システム仕様およびそのGrasping Objects（剛体把持機能）」から抽出する．

構成要素の仕様を詳細に対応づける．それにより提案手法に

3.4. モデル検査

おける連携動作に関する仕様の抽出および連携動作が満たす

産業用ロボットにおける構成要素の連携動作に関する仕様

べき性質の抽出の精度を向上させるためである．策定したシおよび連携動作が満たすべき性質をインプットとしてモデル

ステム仕様書を基にして提案手法を適用した．本節では提案

検査を実施する．モデル検査のアウトプットは，連携動作に手法のフローに沿って提案手法の適用内容を述べる．

関する不整合内容もしくは連携動作が整合している構成要素(1) アーキテクチャ設計の仕様および構成要素間のインタフェース仕様である．モデ

不定形剛体運搬ロボットシステムのシステム仕様を基に，

ル検査ツールである UPPAAL の表現形式に従い，構成要素

IEEE 1220 に定められるプロセスに従いアーキテクチャ設計の仕様および構成要素間のインタフェース仕様における連携を実施した．アーキテクチャ設計の結果，不定形剛体運搬ロ

動作に関する仕様をモデル化する．また，UPPAAL の表現

ボットシステムの仕様をロボット制御サブシステムの仕様お形式に従い，連携動作が満たすべき性質からモデル検査の検よび形状測定サブシステムの仕様，サブシステム間のインタ査式を作成する．作成したモデルおよび検査式を UPPAAL

フェース仕様に分解した．Fig. 10 に不定形剛体運搬ロボットに入力し，モデル検査を実施する．モデル検査の結果，検査システムのアーキテクチャ設計結果を示す．Fig. 10 にはサ式で表す性質をモデルが満足しない場合，UPPAAL から出

ブシステムの説明のために，サブシステムを構成するコンポ

力される反例を分析し連携動作の不整合内容をアーキテクチ

ーネントを明示している．

ャ設計にフィードバックする．フィードバックした連携動作

ロボット制御サブシステムはつぎに示すコンポーネントでの不整合内容を基に，再度，作業フローに従いアーキテクチ

構成される．

ャ設計を実施する．モデル検査の結果，検査式で表す性質を ロボットハンド

モデルが満足する場合，連携動作が整合している構成要素の ロボットアーム仕様および構成要素間のインタフェース仕様をリリースする．

 ロボット動作のプログラミングや緊急停止を行うティーチペンダント4.

産業用ロボットの開発事例

 ロボットハンドを制御するコントローラ
 ロボットアームおよびティーチペンダントを制御す

本章では，不定形な剛体を運搬する産業用ロボットの開発

るコントローラ

において，提案手法を適用した事例を示す．

 運用者が作業指示やシステムのステータス確認を行

4.1. 不定形剛体運搬ロボットシステム

うコンソール

不定形剛体運搬ロボットシステムとは，形状・寸法が一定

 ロボット制御サブシステムの統合制御を行うロボッ

ではない重量のある剛体の把持，運搬，据置を行う産業用ロ

ト制御計算機

ボットである．不定形剛体運搬ロボットシステムの特徴は，ロボット制御計算機はつぎに述べる形状測定サブシステムと不定形剛体の把持および据置作業に対してつぎに示す強い自のインタフェースを有する．

律性が求められる点である．不定形剛体運搬ロボットシステ

形状測定サブシステムはつぎに示すコンポーネントで構成

ムにおいて不定形剛体を把持する領域は限定されているものされる．

の，剛体の形状・寸法，剛体を把持する位置，剛体の姿勢は剛体ごとに変化する．システムは剛体を把持するにあたり剛

Robot System Specification
for Carrying Indeterminate-form and Rigid Objects

体の形状・寸法，位置，姿勢を正確に知る必要がある．また

Sub-System Specification
for Controlling Robot

不定形剛体を据え置く領域は限定されているものの，その領域の中で剛体を据え置く位置が変化する．システムは剛体を

Sub-System Specificationfor Sensing Shape
ComputerComputer for
for
Controlling
Controlling
Sensing
Sensing

ConsoleConsole据え置くにあたり他の剛体が存在しない位置もしくは剛体が敷き詰められた領域において最も標高が低い位置を正確に知ComputerComputer for
for
Controlling
Controlling Robot
Robot

Interface Specificationfor Sub-Systems

る必要がある．
4.2. 提案手法の適用

Controller
Controller

Laser
Laser
Scanner
Scanner

VerticalVertical Motion
Motion Mechanism
Mechanism
forfor Laser
Laser Scanner
Scanner

Controller
Controller

不定形剛体運搬ロボットシステムを開発するにあたり，まRobot
Robot Hand
Hand

ず開発要求を基にシステムの要求分析を実施した．システム

Robot
Robot Arm
Arm

Teaching
Teaching
Pendant
Pendantの要求分析を実施することで不定形剛体運搬ロボットシステ
Systemムのシステム仕様を確定しシステム仕様書を策定した．シス

Sub-System

Component

Fig. 10 Results of Architectural Design
42Interface

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

アームおよびロボットハンドを制御し剛体の把持を行うこと．

 3 次元形状を測定するレーザスキャナ
 レーザスキャナ上下動機構

3.1.1.1.f 剛体の把持を完了した場合，剛体把持要求の結 レーザスキャナおよびレーザスキャナ上下動機構を

果をコンソールに出力すること．

制御する測定制御計算機

形状測定サブシステム仕様

測定制御計算機はロボット制御サブシステムとのインタフェ

6.1.1.1.1.aースを有する．

ロボット制御サブシステムから剛体測定要求を受信すること．
剛体測定要求を受信した場合，剛体の測定

形状測定サブシステムは剛体を把持する際に剛体の形状・6.1.1.1.2.a

寸法，位置，姿勢を測定する．剛体を据え置く際に据置領域の凹凸状況を測定する．形状測定サブシステムはロボット制を開始すること．
レーザスキャナを測定開始位置に移動する

御サブシステムに対して測定した情報を送信する．ロボット

6.1.2.1.a

制御サブシステムは形状測定サブシステムからの情報を基に，こと．
6.1.2.1.b
レーザスキャナを用いて剛体を測定し剛体

不定形剛体の把持，運搬，据置を行う．

の標高データを取得すること．
6.1.2.1.c
剛体の標高データの取得時点におけるレー

アーキテクチャ設計の結果を基にロボット制御サブシステ
ムおよび形状測定サブシステムの仕様書を策定した．それら

ザスキャナの上下位置を取得すること．
6.1.2.1.d
剛体に対する 1 走査分の標高データの取得

サブシステム仕様書の策定においても仕様の 1 つ 1 つに対して項番を付与した．

が終了した場合，レーザスキャナの上下位置をθ度進めること．

また，アーキテクチャ設計の過程においてロボット制御サブシステムおよび形状測定サブシステムに関するトレーサビ
リティマトリクスを作成した．トレーサビリティマトリクス

6.1.2.1.e

レーザスキャナの上下位置がψからφ度における標高データを測定すること．

6.1.2.1.f

レーザスキャナの上下位置，その位置における剛体の標高データがマトリクスになった測の作成においては仕様 1 つ 1 つに付与した項番単位で不定形
剛体運搬ロボットシステムの仕様とロボット制御サブシステ
ムおよび形状測定サブシステムの仕様との対応関係をまとめた．
6.1.3.1.a(2) 構成要素の連携動作に関する仕様の抽出

定 CSV データを作成すること．
測定 CSV データを基に剛体の測定データを算出すること．
剛体測定要求に対する測定処理が正常に終

トレーサビリティマトリクスを基にロボット制御サブシス

6.1.1.2.1.a

テムの仕様および形状測定サブシステムの仕様，サブシステ了した場合，ロボット制御サブシステムに対して測定データおよびエラー種別（正常）を送信

ム間のインタフェース仕様から連携動作に関する仕様を抽出した．連携動作に関する仕様の抽出について，その一例を示すること．
6.1.1.2.1.b
剛体測定要求に対する測定処理においてエす．つぎに示す仕様はそれぞれの仕様書からの抜粋で設計情報を抽象化している．4 章 2 節 (1)で述べたトレーサビリテ

ラーが発生した場合，ロボット制御サブシステ
ムに対して該当するエラー種別を送信すること．

ィマトリクスにおいて不定形剛体運搬ロボットシステムの仕様 6.1.8.2.a はロボット制御サブシステムの仕様 3.1.1.1.a から
3.1.1.1.f，形状測定サブシステムの仕様 6.1.1.1.a から 6.1.3.1.a

またこれらの連携動作に関する仕様においてサブシステム間に対応付けられる．

のインタラクション情報として剛体測定要求および剛体測定応答に着目する．サブシステム間のインタフェース仕様にお不定形剛体運搬ロボットシステム仕様
6.1.8.2.a 一定の位置に据え置かれている剛体を見出し把いてこれらのインタラクション情報に対応する仕様をつぎに持すること．

示す．仕様に対応する番号はサブシステム間のインタフェー

ロボット制御サブシステム仕様

ス仕様に付与された項番である．

3.1.1.1.a コンソールからの剛体把持要求を待つこと．

サブシステム間インタフェース仕様

3.1.1.1.b 剛体把持要求を受信した場合，剛体測定要求を

4.1

物理インタフェース

4.2.2.1

3.1.1.1.c 作成した剛体測定要求を測定制御サブシステム

4.2.3

剛体測定要求／応答シーケンス
データ定義に対して送信すること．
3.1.1.1.d 剛体測定要求を送信後，測定制御サブシステム

4.2.4.1

剛体測定要求／応答メッセージフォーマット

作成すること．

連携動作に関する仕様の抽出について，以上に示す手順にからの剛体測定応答の受信待ちを行うこと．
3.1.1.1.e 形状測定サブシステムから剛体測定応答を受信よりロボット制御サブシステム仕様における仕様 78 項目かした場合，剛体測定応答の内容を基にロボットから 23 項目を抽出した．また，サブシステム間のインタフ

ら 12 項目，形状測定サブシステム仕様における仕様 58 項目
ェース仕様における仕様 26 項目から 22 項目を抽出した．

43

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

以内に不定形剛体運搬ロボットシステムの動作を停止すること．

(3) 構成要素の連携動作が満たすべき性質の抽出
トレーサビリティマトリクスを基に，不定形剛体運搬ロボ
ットシステムのシステム仕様からロボット制御サブシステム

4 章 2 節 (2)で示すロボット制御サブシステムおよび形状および測定制御サブシステムによる連携動作が満たすべき性

測定サブシステムによる連携動作の仕様はこれらのシステム

質を抽出した．連携動作が満たすべき性質の抽出について，仕様を満たす必要がある．ここで，これらのシステム仕様を

その一例を示す．つぎに示す仕様は不定形剛体運搬ロボット

ロボット制御サブシステムおよび形状測定サブシステムの設システムの仕様書からの抜粋で設計情報を抽象化している．

計情報で置き換える．これらのシステム仕様から抽出したロ

4 章 2 節 (2)に示すロボット制御サブシステムおよび形状測ボット制御サブシステムおよび形状測定サブシステムによる

定サブシステムの連携動作に関する仕様は，4 章 2 節 (2)で連携動作が満たすべき性質をつぎに示す．P.1-5 および P.3-3示す不定形剛体運搬ロボットシステムの仕様以外につぎの仕は，それぞれの性質に付与した番号である．

不定形剛体運搬ロボットシステムを構成する装ロボット制御サブシステムは，形状測定サブシ
ステムに対する剛体測定要求に対し，形状測定

置間におけるデータ送受信は要求／応答方式を採用すること．

サブシステムから剛体測定結果もしくは剛体測
定失敗の応答を受信すること．

P.1-5様に対しても対応付けられる．
5.5.2

6.3.2.cコンソールからの動作停止要求に対してｔms

P.3-3

形状測定サブシステムは，ロボット制御サブシ

R.1-5

R.1-5

Fig. 11 Cooperating Behavior Model on Sub-System for Controlling Robot44

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

ステムによる測定停止要求の送信後 100ms 以
内に測定処理を停止すること．

するイベントを識別する．前述の連携動作に関する仕様の場
合，「測定処理の正常終了」がイベントである．これが状態

連携動作が満たすべき性質の抽出について，以上に示す手

遷移モデルにおける状態の遷移条件となる．そして連携動作

順により 23 項目を抽出した．

に関する仕様の中から状態遷移に関するアクションを識別す(4) モデル検査

る．前述の連携動作に関する仕様の場合，「ロボット制御サ

ロボット制御サブシステムの仕様および測定制御サブシス

ブシステムに対して測定データおよびエラー種別（正常）をテムの仕様，サブシステム間のインタフェース仕様から抽出

送信」がアクションである．これが状態遷移モデルにおけるした連携動作に関する仕様を基に，UPPAAL の表現形式に

状態遷移時に行う手続きとなる．

従い連携動作のモデルを作成した．Fig. 11 から Fig. 13 に連

また，UPPAAL の表現形式に従いロボット制御サブシス

携動作のモデルを示す．作成したモデルは連携動作において

テムおよび測定制御サブシステムによる連携動作が満たすべ

ロボット制御サブシステムに対応するモデル（Fig. 11），形

き性質を基に検査式を作成した．検査式を作成するにあたり状測定サブシステムに対応するモデル（Fig. 12），サブシス

非形式的に表現される満たすべき性質を基に時相論理によるテム間のインタフェースに対応するモデル（Fig. 13）である．

正確な検査式を作成する Spec Pattern17）を適用した．Spec

UPPAAL による連携動作のモデルは連携動作の状態遷移をPattern は満たすべき性質の中に現れるパターンおよびスコ表現する．状態遷移モデルを作成するにあたり，まず連携動ープとそれらに対応する時相論理表現とのマッピングを提供

作に関する仕様の中から「～待ち」や「～中」などを識別すしている．スコープとは global（常に），before（～の前る．4 章 2 節 (2)に示す形状測定サブシステムの連携動作にに），after（～の後に）などモデル検査の対象となるシステ

関する仕様 6.1.1.2.1.a「剛体測定要求に対する測定処理が正ムの時系列においてある状態やイベントが生じる範囲を定め

常に終了した場合，ロボット制御サブシステムに対して測定たものである．パターンとは absence（ある状態やイベント

データおよびエラー種別（正常）を送信すること」の場合，が指定されたスコープ内で決して生じないこと），その仕様には「剛体測定要求に対する測定処理を実施中」とuniversality（ある状態やイベントが指定されたスコープ内でいう振る舞いが含まれる．これが状態遷移モデルにおける状常に生じること），response（指定されたスコープ内で 1 つ態となる．つぎに連携動作に関する仕様の中から状態に関連

目の状態やイベントの発生後に 2 つ目の状態・イベントが常

R.1-5

R.1-5

R.1-5

R.1-5

R.1-5

R.1-5

Fig. 12 Cooperating Behavior Model on Sub-System for Sensing Shape45

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)に生じること）などスコープにおける状態やイベントの出設計の結果，R.1-5 については形状測定サブシステムおよび

現・順序形態を表したものである．Spec Pattern を用いるこ

測定制御サブシステムの仕様に対してロボット制御サブシスとで時相論理表現に精通していない技術者であっても正確なテムおよび形状測定サブシステムにおける要求・応答を対応

検査式を作成することができる．ロボット制御サブシステム

付ける機能を追加した．R.3-3 についてはロボット制御サブ

および形状測定サブシステムによる連携動作が満たすべき性

システムからの測定停止要求を常に受信できるように形状測質に対して Spec Pattern を適用することで 23 ケースの検査式

定サブシステムの仕様を変更した．また，測定停止要求を受を作成した．前述の連携動作が満たすべき性質 P.1-5 および信した際は直ちに測定を停止し，要求待ち状態に遷移するよ

P.3-3 に対応する検査式をつぎに示す．F.1-5 および F.3-3 は，うに形状測定サブシステムの仕様を変更した．その後，連携それぞれの検査式に付与した番号である．

動作の不整合が解決されたロボット制御サブシステムの仕様

F.1-5
F.3-3

A[] (bing_syscont_sendreq == bing_req_rod)

および形状測定サブシステムの仕様，サブシステム間のイン

imply (bing_syscont_req == bing_req_rod)

タフェース仕様をリリースした．

A[] P_BING_SCAN.BING_SCAN_REQ_STOP

4.3. 適用結果

imply (bing_stopreq_time <= 10)

不定形剛体運搬ロボットシステムの開発において，提案手法

Fig. 11 から Fig. 13 に示す連携動作モデルおよび F.1-5 およを適用した．その結果，不定形剛体運搬ロボットシステムのび F.3-3 を含む 23 ケースの検査式を基に，UPPAAL によるシステム仕様から，ロボット制御サブシステムの仕様およびモデル検査を実施した．モデル検査の実施後，UPPAAL に形状測定サブシステムの仕様，サブシステム間のインタフェより出力された反例を分析した．分析の結果，F.1-5 およびース仕様を見出した．また，これらの仕様を確定する前に，

F.3-3 の検査式の結果を含む 6 ケースの不整合を検出した．

R.1-5 および R.3-3 に示す連携動作の不整合を検出すること

F.1-5 および F.3-3 に対応する連携動作の不整合をつぎに示す．

ができた．その後，連携動作が整合しているロボット制御サ

R.1-5 および R.3-3 は，F.1-5 および F.3-3 に対応する連携動ブシステムの仕様および形状測定サブシステムの仕様，サブ作の不整合内容に付与した番号である．R.1-5 については，

システム間のインタフェース仕様を作成することができた．

Fig. 11 および Fig. 12 において連携動作に関する不整合が混産業用ロボットの開発において提案手法を適用し，産業用ロ

入した箇所を点線で示す．

ボットの高信頼化に貢献した．

R.1-5

メッセージおよび処理のタイミングによって

5.

は，n 回目に発行された剛体測定要求に対して
n 回目より前に発行された剛体測定要求，もし本章では産業用ロボットに対する提案手法の有効性を示す．

くは据置領域測定要求，もしくは測定停止要求に対する応答が返却される場合がある．
R.3-3

考察

また，提案手法の課題を述べる．
5.1. 産業用ロボットに対する提案手法の有効性

測定停止要求に対して 100ms 以内に測定処理が停止しない場合がある．また，測定停止要求

4 章で示した開発事例を基に，提案手法の有効性を示す．
提案手法の有効性を示すにあたり，開発事例における QCDに対して測定サブシステム自体が停止する場合がある．

（Quality：開発対象の品質，Cost：開発コスト，Delivery：開発期間）に着目する．

アーキテクチャ設計に対して R.1-5 および R.3-3 を含む 6

まず，開発対象の品質という観点から提案手法を考察する．

ケースの連携動作の不整合内容をフィードバックした．そし今回，不定形剛体運搬ロボットシステムという機能的に複雑て，再度アーキテクチャ設計を実施した．再アーキテクチャ

な産業用ロボットの開発において提案手法を適用した．そのFig. 13 Cooperating Behavior Model on Interface between Sub-System of Controlling Robot and Sensing Shape46

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

Table. 1 Costs on Applying the Proposed Methodology

結果，ロボット制御サブシステムおよび形状測定サブシステ
ムにおける連携動作の不整合をアーキテクチャ設計に対してフィードバックし，1 回の反復で連携動作が整合しているロボット制御サブシステムの仕様および形状測定サブシステム

No.

Work

Cost（man‐hours）

1

Architectural Design－

2

Extraction of Specification for
Cooperating Behavior
among Elements

2

3

Identification of Properties for
Cooperating Behavior
among Elements

24Model Checking

12の仕様，サブシステム間のインタフェース仕様を作成することができた．特に本論文 4 章 2 節の R.1-5 および R.3-3 に示す連携動作の不整合については，満たすべき性質が成り立つかどうかをしらみつぶしに確認するモデル検査ならではの人
手では検出することが困難な不具合といえる．そのような不具合を産業用ロボット開発の上流工程で検出できたことは，提案手法における有効性の表れである．
つぎに，開発コストおよび開発期間という観点から提案手システム試験において本不具合が検出されると仮定した場合，法を考察する．Table. 1 に開発事例に対して提案手法を適用した際の工数を示す．本論文ではアーキテクチャ設計を除く

それらの改修に 40 人日の工数を要する可能性がある．これ作業で要した工数をまとめる．システム開発においてアーキ

は不定形剛体運搬ロボットシステムの全開発工数の約 10%に相当する．したがって，システム開発全体で考えた場合，テクチャ設計を含むシステムエンジニアリング手法を適用す

構成要素の連携動作に関する仕様の抽出，構成要素の連携動

18）～21）

る効果については，多くの先行研究が存在する．こ作が満たすべき性質の抽出，モデル検査に要する工数は，費れらの先行研究ではシステムエンジニアリング手法を適切に

用対効果の高い工数であると考える．

適用することで，システム開発における開発コストの削減および開発期間の短縮が可能であることが示されている．本論

5.2. 課題文においては，今回の開発事例に対してアーキテクチャ設計

本論文 5 章 1 節において，産業用ロボットに対する提案手法の有効性を確認することができた．しかし，提案手法には手法を適用した際の開発コストの削減および開発期間の短縮

解決すべき課題がある．提案手法は構成要素の連携動作が整の程度を示すことはできない．しかし，前述の通りアーキテ

合していることを確認するためにモデル検査を採用している．

クチャ設計において確実な成果が得られたことを考慮した場

モデル検査においてモデルの状態数が多い場合，状態の組み合，システム開発における開発コストの削減および開発期間

合わせが膨大になることでモデル検査が終了しない状態爆発の短縮を実現した可能性が高い．また，構成要素の連携動作という現象が発生することがある．アーキテクチャ設計の結に関する仕様の抽出については 2 人時間，構成要素の連携動果，構成要素の連携動作が極端に複雑になると状態爆発によ作が満たすべき性質の抽出については 2 人時間，モデル検査

りモデル検査による連携動作の検証が終了しない可能性があについては 12 人時間の工数を要した．不定形剛体運搬ロボ

る．その場合，構成要素による連携動作が極端に複雑にならットシステムを開発するにあたり，7 人時間を 1 人日とした

ないように再度アーキテクチャ設計を実施する方策や連携動場合に全体で 498 人日の工数を要した．構成要素の連携動作

作の仕様に関するモデルの状態数を減らす方策などが必要にに関する仕様の抽出，構成要素の連携動作が満たすべき性質なる．ただしシステム設計段階におけるこれらの工数の増大の抽出，モデル検査に要した工数の合計 14 人時間（2 人は，5 章 1 節で述べた通りシステム開発全体では費用対効果日）は，不定剛体運搬ロボットシステムの開発全体に要したの高い工数であると考える．また不定形剛体運搬ロボットシ

工数の 0.4%程度である．また，サブシステム間における連携動作の不整合について，一般にそれらを検出することが可ステムに対する提案手法の適用では UPPAAL の実行環境と能な開発フェーズは，システム開発の終盤に実施されるサブ

してクロック周波数 1.86GHz，メモリ 2.96GB を搭載する計システム同士を組み合わせたシステム試験である．システム

算機を使用した．その環境において Fig.11 から Fig.13 に示試験においてサブシステム間における連携動作の不整合を検した連携動作モデルおよび 4 章 2 節 (4)で述べた F.1-5 および出した場合，その改修に多くの改修コストおよび改修期間を

F.3-3 を含む 23 ケースの検査式によるモデル検査を実施した．
その結果，それぞれのケースに対する検査は高々1 秒以内に要する．文献22）の中で Boehm は，要求仕様の段階で要求終了した．本結果から 4 章 2 節 (2)の連携動作に関する仕様の誤りを検出し修正する際のコストを 1 とした場合，試験にで示した連携動作の複雑度を有する産業用ロボットの開発においては小規模システムで 2，大規模システムで 20 のコス

おいては状態爆発が発生しないことを確認することができた．

トを要すると分析している．本論文 4 章 2 節の R.1-5 および
R.3-3 に示す連携動作の不整合は，要求仕様を確定する段階
においてモデル検査を適用しない限り見逃される可能性がある不具合といえる．システム設計段階において提案手法により検出した不具合を改修するにあたり 2 人日の工数を要した．

47

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)

した課題の解決を通して，更に品質の高い開発手法の確立を

6.

関連研究

図る．

産業用ロボットの信頼性を向上させる取り組みとして，ロ

参考文献

ボット開発にモデル検査を適用する方法が提案されている．

1） 日本工業標準調査会：産業用マニピュレーティングロボ

M. Kim らは Esterel 言語23）を用いて形式的に定義されたロボット－用語，JIS B 0134（2008）

ットの設計仕様に対し，Esterel 言語に対応したモデル検査ツ2） 社団法人日本ロボット工業会：世界の産業用ロボット稼ールである XEVE24）を用いてモデル検査を実施する手法を

動台数，社団法人日本ロボット工業会（オンライン），

提案している25）．また，N. Trcka らは Chi 言語26）を用いて入手先< http://www.jara.jp/data/dl/kado.pdf >（参照 2010-

形式的に定義されたロボットの設計仕様をモデル検査ツール

03-16）SPIN27）のモデリング言語である PROMELA27）に変換し，

3） 矢内重章：産業用ロボットの現状と将来展望，生産と電SPIN によるモデル検査を実施する手法を提案している28）．

気，61-3，36/41（2009）

これらの提案手法は，モデル検査の適用により産業用ロボッ

4） 榊原伸介：産業用ロボットの最新技術動向，ロボット，

トにおける信頼性を向上させる可能性がある．しかし，これ

180，4/9（2008）

らの提案手法はロボットの構成要素による連携動作に着目していない．ロボットハンドやロボットアーム，センサなどの

5） 加藤淳，浦郷正隆，狼嘉彰：複雑システムの信頼性を向構成要素が連携することで満たすべき機能を実現する産業用

上させる開発手法：アーキテクチャ設計手法とモデル検ロボットにおいては，構成要素による連携動作の信頼性を向査の融合，Synthesiology，3-3,，197/212（2010）

上させることが重要である．

6） Institute of Electrical and Electronics Engineers (IEEE): IEEE

本論文における提案手法と同様に，ロボットの構成要素にStandard for Application and Management of the Systems

よる連携動作に着目した先行研究も存在する．N. C. W. M.

Engineering Process, IEEE 1220-2005 (2005)

Braspenning らは前述の Chi 言語を用いてロボットの各構成

7） K. G. Larsen, P. Pettersson and W. Yi: UPPAAL in a nutshell,

要素における設計解をモデル化し，各構成要素のモデルを結International Journal on Software Tools for Technology

合することで Chi システムモデルを作成している．そして，

Transfer, 1, 134/152 (1997)

Chi システムモデルをモデル検査ツールである UPPAAL のモデルに変換しモデル検査を実施する手法を提案している29）．
産業用ロボットの開発において N. C. W. M. Braspenning らの

8） E. M. Clarke, O. Grumberg and D. E. Long: Model Checking
andabstraction,

ACM

Transactionson

Programming

Languages and Systems, 16-5, 1512/1542 (1994)

提案手法を適用することで，実プロダクトを結合する前に構

9） International Council on Systems Engineering (INCOSE):

成要素による連携動作の不整合を検出できる可能性がある．

INCOSE SYSTEMS ENGINEERING HANDBOOK version

しかし，この提案手法は構成要素の仕様を基に導出された設

3.1, 1.5 of 6, INCOSE, USA (2007)

計解を対象としている．ロボットのシステム仕様からロボッ

10）トの構成要素に対して仕様が正しく分割されていることを前

T. Doran: IEEE 1220: for practical systems engineering,IEEE Computer, 39-5, 92/94 (2006)

提としている．構成要素の実プロダクトを結合する直前に連11）

携動作の不整合を検出するため，開発の上流工程に対する手J. A. Estefan: Survey of Model-Based Systems

戻りのインパクトが大きくなる可能性がある．産業用ロボッ

Engineering (MBSE) Methodologies, International Council onトの開発においては，構成要素による連携動作を確実に設計

Systems Engineering (INCOSE) MBSE Focus Group (2007)

し，開発の上流工程において連携動作の整合を確認すること

12）

E. M. Clarke and J. M. Wing: Formal methods: state of

the art and future directions, ACM Computing Surveys, 28-4,が重要である．

626/643 (1996)

7.

まとめ

13）

M. Sipser: Introduction to the Theory of Computation,

Chapter 1, Course Technology Ptr(SD), The Netherlands

本論文では，産業用ロボット開発の上流工程であるシステ(1996)

ム設計段階において，産業用ロボットのシステム仕様を連携

14）動作が整合している産業用ロボットにおける構成要素の仕様

R. Alur and D. L. Dill: A theory of timed automata,

Theoretical Computer Science, 126-2, 183/235 (1994)

および構成要素間のインタフェース仕様に分解する開発手法

15）の実例および産業適用の具体例を示した．提案手法の適用結E. M. Clarke, E. A. Emerson and A. P. Sistla: Automatic

果から産業用ロボットに対する提案手法の有効性を示した．

Verification of Finite-State Concurrent Systems Using

ただし，提案手法には改善の余地もある．今後，本論文で示

Temporal Logic Specifications, ACM Transactions on
Programming Languages and Systems, 8-2, 244/263 (1986)48

計測自動制御学会産業論文集
Vol.10, No.5, 37/49 (2011)16）

G. Behrmann, A. David, and K. G. Larsen: A tutorial on

29）

N. C. W. M. Braspenning, E.M. Bortnik, J. M. van de

UPPAAL, Proceedings of Formal Methods for the Design ofMortel-Fronczak and J. E. Rooda: Model-based system

Real-Time Systems(SFM-RT 2004), 3185 of Lecture Notes inanalysis using Chi and Uppaal: An industrial case study,

Computer Science, 200/236 (2004)

Computers in Industry, 59-1, 41/54 (2008)

17）

M. B. Dwyer, G. S. Avrunin and C. Corbett: Pattern in

Property

Specification

for

Finite-State

著者紹介

Verification,

Proceedings of the 21th International Conference on Software
加藤

Engineering, 411/420 (1999)

淳

J. P. Elm: A study of Systems Engineering Effectiveness2000 年熊本大学大学院自然科学研究科電– Initial Results, Proceedings of the Systems Conference 2008

気システム専攻修了．同年より電機メ2nd Annual IEEE, 1/7 (2008)

ーカにおいて，ユビキタス環境におけ

18）

19）

る小型ネットワークデバイスの研究・

B. Boehm, R. Valerdi and E. Honour: The ROI of

開発業務などに従事．2006 年より宇宙Systems Engineering: Some Quantitative Results for Software-

業界において，宇宙機ソフトウェアのIntensive Systems, Systems Engineering, 11-3, 221/234 (2008)20）

独立評価業務に従事．また，慶應義塾大学大学院システ

E. C. Honour: Understanding the Value of Systems

ムデザイン・マネジメント研究科において，システムエ

Engineering, Proceedings of the INCOSE International

ンジニアリングに関する研究に取り組む．2009 年情報処

Symposium, 1-16 (2004)
21）

理学会研究賞受賞．情報処理学会会員．

A. K. Kludze: The Impact of Systems Engineering onComplex Systems, Proceedings of Conference on Systems

浦郷

Engineering Research (2004)
22）

正隆
1998 年東京工業大学大学院理工学研究科

B. W. Boehm: Software Engineering Economics, 38-40,

機械物理工学専攻博士課程修了．博士

PRENTICE-HALL, USA (1981)23）（工学）．同年より東京工業大学で助G. Berry and G. Gonthier: The Esterel synchronous

手を務める．2008 年より慶應義塾大学

programming language: Design, semantics, implementation,

大学院システムデザイン・マネジメン

Science of Computer Programming 19-2, 87/152 (1992)
24）

A.

Bouali:XEVE,

an

ESTERELト研究科准教授となる．システムズエンジニアリングおよび工学問題のコンピュータモデリング，数値計算に関VerificationthEnvironment, Proceedings of the 10 International Conferenceする研究に取り組む．日本機械学会会員．INCOSE 会員．

on Computer-Aided Verification (CAV’98), 1427 of Lecture

日本計算数理工学会会員．

Notes in Computer Science, 500/504 (1998)
25）

狼

M. Kim, K. C. Kang and H.Lee: Formal Verification of

嘉彰（正会員）

Robot Movements – a Case study on Home Service Robot

1968 年東京工業大学大学院理工学研究科

SHR100, Proceedings of the 2005 IEEE International

電気工学専攻修了．工学博士．NASA

Conference on Robotics and Automation (ICRA), 4739/4744

国際フェロー，東京工業大学教授，慶(2005)

應義塾大学教授，宇宙開発事業団技術26）

研究本部研究総監を経て，2008 年より

D. A. Ban Beek and J. E. Rooda: LANGUAGES ANDAPPLICATIONSINHYBRID

MODELLING

慶應義塾大学大学院システムデザイ

ANDン・マネジメント研究科委員長を務める．複雑システム

SIMULATION: POSITIONING OF CHI, Control Engineeringのダイナミクス・制御および戦略的システムエンジニア

Practice, 8-1, 81/91 (2000)
27）

リングに関する研究に取り組む．計測自動制御学会産業

G. J. Holzmann: The Model Checker SPIN, IEEE

論文 Associate Editor．日本機械学会フェロー．INCOSE

Transactions on Software Engineering, 23-5, 279/295 (1997)28）

フェロー．日本航空宇宙学会会員．IEEE 会員．AIAA 会

N. Trcka: Verifying Chi Models of Industrial Systems

員．ASME 会員．

with Spin, Proceedings of the 8th International Conference on
Formal Engineering Methods (ICFEM’06), 4260 of Lecture
Notes in Computer Science, 132/148 (2006)49