コンピュータソフトウェア2006年特集号「システム検証の科学技術」 同期

http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
コンピュータソフトウェア2006年特集号「システム検証の科学技術」
同期型言語を用いたソフトウェア検証：
クルーズコントロールシステムにおける事例紹介（付録）
足立 正和†，富永 孝‡，佐野 範佳‡，潮 俊光†
2006年７月
† 大阪大学大学院基礎工学研究科
‡ 豊田中央研究所
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
2/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
入出力一覧
表1.入力表
内容
メインSW
セットSW
リジュームSW
キャンセルSW
車間距離切替SW
セット車速増速SW
セット車速減速SW
現車速
先行車有無
相対速度
車間距離
アクセルペダル
ブレーキペダル
シフト操作(D,S以外に変更)
センサ不良
VSC作動
システム異常
2006/07
2006/07
名
MainSW
SetSW
ResumeSW
CancelSW
DistanceChange
GainButton
SlowDownButton
VehicleSpeed
PrecedCar
RelativeSpeed
VehicleDistance
AccelPedal
BrakePedal
ShiftOperate
SensorError
VSCOperate
SystemError
型
Boolean
Boolean
Boolean
Boolean
Boolean
Boolean
Boolean
Real
Boolean
Real
Real
Boolean
Boolean
Boolean
Boolean
Boolean
Boolean
表2.出力表
内容
制御中状態
スタンバイ状態
制御中断状態
制御禁止状態
加速状態
減速状態
定速状態
CruiseONモード
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
名
CruiseAction
CruiseStandby
CruseBreak
CruiseFail
AccelState
BrakeState
UniformState
CruiseOn
型
Boolean
Boolean
Boolean
Boolean
Boolean
Boolean
Boolean
Boolean
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
3/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
変数・定数一覧
表3.内部変数表
内容
ユーザキャンセル条件成立
システムキャンセル条件成立
システム異常発生
制御車間距離
セット車速
加速イベント
減速イベント
名
UserCancel
SystemCancel
SystemFail
CruiseDistance
CruiseSpeed
AccelEvent
BrakeEvent
型
Boolean
Boolean
Boolean
Real
Real
Boolean
Boolean
定数名
CruiseSpeedMax
CruiseSpeedMin
SpeedUp
SpeedDown
Zero
型
表4.定数表
内容
セット上限
セット下限
セット車速増加変動値
セット車速減少変動値
零値
2006/07
2006/07
real
real
real
real
real
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
値
100
40
5
5
0
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
4/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
モデル全体図
1
16
MainSW
CruiseBreak
CruiseON
CruiseControl
Sy stMgt
4
CruiseFail
CruiseAction
AccelPedal
6
CruiseStandby
2
SetSW
VehicleDistance
5
15
Relativ eSpeed
16
AccelState
ResumeSW
BrakePedal
12
CruiseControlState
Mgt
17
SetSW
PrecedCar
CancelSW
GainButton
SensorError
AccelPedal
Cancel
SlowDownButton
CruiseSpeed
Mgt
DistanceControl
VSCOperate
BrakeState
VehicleSpeed
VehicleSpeed
Shif tOperate
Sy stemError
3
Unif ormState
VehicleSpeed
12
CruiseDistance
DistanceChange
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
5/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
1. CruiseControlSystMgt
MainSW
CruiseON
Cruise ON モード決定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
6/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
2. Cancel
AccelPedal
13
BrakePedal
UserCancel
UserCancel
CancelSW
Shif tOperate
Sy stemError
Sy stemFail
9
SensorError
Sy stemCanc
el
Sy stemCancel
VSCOperate
VehicleSpeed
キャンセル条件設定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
7/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
2-1. UserCancel
AccelPedal
BrakePedal
UserCancel
CancelSW
Shif tOperate
ユーザキャンセル条件設定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
8/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
2-2. SystemCancel
SensorError
Sy stemCancel
VSCOperate
VehicleSpeed
CruiseSpeedMin
システムキャンセル条件設定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
9/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
3. CruiseDistance
1
51
DistanceModeMgt
DistanceChange
1
CruiseDistan
ceValue
CruiseDistance
VehicleSpeed
制御車間距離変更
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
10/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
3-1. DistanceModeMgt
制御車間距離コントローラ
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
11/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
3-2. CruiseDistanceValue
Distance_Middle
Distance_Long
0.45
0.33
0.6
CruiseDistance
3.5
VehicleSpeed
制御車間距離算出
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
12/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
4. CruiseControlStateMgt
制御状態決定コントローラ
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
13/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
5. CruiseSpeedMgt
1
RisingEdge
_FirstStep
CruiseAction
SetSW
7
VehicleSpeed
GainButton
10
CruiseSpeed
Change
L
H
CruiseSpeed
SlowDownButton
CruiseSpeedMin
CruiseSpeedMax
1
FBY
セット車速変更
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
14/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
5-1. CruiseSpeedChange
65
GainButton
66
CruiseSpeed_IN
SlowDownButton
SpeedUp
CruiseSpeed
SpeedDown
Zero
セット車速増減操作
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
15/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
6. DistanceControl
VehicleDistance
1
1
DistanceCont
rolEv ent
CruiseDistance
AccelState
DistanceControlSta
teDecide
Relativ eSpeed
Decision
BrakeState
PrecedCar
Unif ormState
AccelPedal
VehicleSpeed
CruiseAction
CruiseSpeed
車間維持制御・加減速状態決定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
16/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
6-1. DistanceControlEvent
VehicleDistance
CruiseDistance
AccelEv ent
BrakeEv ent
Zero
Relativ eSpeed
Zero
Zero
加減速イベント決定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.
17/17
http://ushiolab.sys.es.osaka-u.ac.jp/ut/scade/acc.html
6-2. Distance Control State Decision
BrakeEv ent
f alse
BrakeState
VehicleSpeed
PrecedCar
AccelPedal
Unif ormState
AccelEv ent
AccelState
CruiseSpeed
加減速状態前提条件判定
2006/07
2006/07
Graduate
Graduate School
School of
of Engineering
Engineering Science,
Science, Osaka
Osaka University.
University.
Toyota
Toyota Central
Central R&D
R&D Labs.,
Labs., Inc.
Inc.