KAOS 1 1 1 1 1,.,. ( ). KAOS VDM++.,.,,, 1. 1.1,, [1].,,, [2].,, [3]. 1.2 ( ),, [3] KAOS, VDM++, KAOS VDM++ 1 Kyushu University, KAOS,, KAOS, KAOS, VDM++., 1.3 2,., 3, KAOS VDM++. 4, 3,. 5 2. 2.1,,,,, 2.1.1 VDM VDM(Vienna Development Method) 1, 1960 IBM [4].VDM VDM-SL,VDM++,VDM-RT 3 1
VDM-SL ISO.VDM++ VDM-SL VDM- RT VDM++ VDM,.VDM, [5]. VDM++. 2.1.2 VDM++.,,, [7]., VDM++.,., [7]. 2.1.3 VDM++.,,,,,,,.,,, 2.1.4 VDM VDMTools OvertureTool VDM.VDMTools IFAD.2005 SCSK CSK, [4].OvertureTool Eclipse, Peter Gorm Larsen [8]., KAOS VDM++ 2.2 [9].,. 2.2.1 KAOS KAOS(Knowledge Acquisition in automated Specifications) Lamsweerde [3].KAOS,,, [10]...,,.., 2.2.2 KAOS Objectiver Respect-IT KAOS [11].KAOS, KAOS, Objectiver KAOS 3., KAOS VDM++,.,. 3.1 [3], KAOS VDM++, KAOS, [3],,,,, 2
VDM++, [3] KAOS KAOS, VDM++ 3.2 KAOS 3.1, KAOS [12], KAOS KAOS [3] KAOS 1,, Assignment,, Performance, Control,, is-a, Binary Association, Control Binary Association., VDM++, VDM++ 3.3 KAOS VDM++,,,,,,,,,., [3],., is-a. 3.3.1 [3] is-a, Binary Association, *,,. 3.3.2 VDM++,,, 3,,,,, Binary Association,.,,,,, Control.,,, is-a, Performance,, VDM++ is not yet specified., 3
,, ( ),,,,, ( ),, 1, [ASTER, ] Fig. 1 Hardware of the vending machine, VDM++ 4. 3, CPU,,. 4.1 [13]( ) ASTER [14]( ) ASTER Association of Software Test EngineerRing) [15]. 4.1.1, 1. 4.1.2 5,, 4.2 KAOS,,. 4.2.1 KAOS 2.,,,.,,,,,,,,,, 2,,, 3,,. 4
情報処理学会研究報告 図 2 商品選択ゴールモデル Fig. 2 Goal model for product selection 図 3 販売ボタン責任モデル Fig. 3 Responsibility model for sell button 図 5 販売ボタン操作モデル Fig. 5 Operation model for sell button 図 5 は販売ボタンの操作モデルである. 販売可能ラン プを点滅 という操作は, 入出力エンティティを持た ない. 販売ボタンに対応する商品の通知 という操作 は入力を持たず, 出力としてエンティティ 商品 を 返す. 4.2.2 生成されたクラスファイル 3.2 の変換手法により, 4.2.1 で構築した自動販売機の KAOS モデルから VDM++のクラスファイルを生成した. 共通定義クラス, オブジェクト定義クラスとして 商品 ク 図 4 商品選択オブジェクトモデル Fig. 4 Object model for product selection ラス, エージェント定義クラスとして 自動販売機システ ム クラス, 販売ボタン クラス, 販売ボタン制御 ク ラス, ラック クラス, 金額表示機 クラス, 貨幣処 商品選択ユースケースのゴールモデルから抽出された 理 クラスの合計 8 クラスが生成された. 図 6 は生成され エンティティとエージェント関係を記述した. 図??は た 販売ボタン クラスである. インスタンス変数として 作成したオブジェクトモデルである. 操作モデル 2016 Information Processing Society of Japan 販売可能ランプ と 商品, 操作としてコンストラクタ と 販売可能ランプを消灯, 販売可能ランプを点滅, 5
7 Fig. 7 Corrected class file for sell button 6 Fig. 6 Generated class file for sell button,. 4.2.3,, 7,,., KAOS.,, KAOS,., 1.,,,. 1 Table 1 Result of acquiring formal specification 10 0 1 21 4 0.81 26 4 0.85 15 4 0.73 12 0 1 8 3 0.63 11 2 0.82 12 0 1 115 17 0.85 = 85 4.2.4 (1),, 8 6
Table 2 2 Breakdown list of acquiring formal specification,,,,,,,,, 9 Fig. 9 Goal model for price input 10 Fig. 10 Changed responsibility model for sell button,,. 10.,.,.,, KAOS VDM++, VDM++ 5. 8 4.2.5,,,,, KAOS, 9 5.1 4, 3 KAOS,, KAOS VDM++.,, KAOS, VDM++, VDM++ 4.2.3 3., 7
3 Table 3 The number of additional row 3 3 6 1 2 2 17, KAOS, 1 * (0 ),,. [3] is-a,, KAOS is-a,, VDM++ 5.2, KAOS,, VDM++. KAOS,,, UML, KAOS VDM++,,., KAOS,,, VDM++, VDM++, KAOS VDM++ [5] IPA/SEC:, http://www.ipa.go.jp/files/000026875.pdf, [6] CSK SYSTEMS CORPORATION: VDM++, http://www.vdmtools.jp/uploads/manuals/ langmanpp_a4j.pdf, [7] Bertrand Meyer, : 2,, (2007). [8] Overture Tool Formal Modeling in VDM, http://overturetool.org/, [9] :,, (2007). [10] Recpect-IT: A KAOS Tutorial, http://www.objectiver.com/fileadmin/download/ documents/kaostutorial.pdf, [11] Engineer your requirements with Objectiver, http://objectiver.com/index.php?id=4, [12],, : IMPULSE:KAOS,, Vol. 48, No. 8, pp.2551-2565, (2007). [13] ASTER: ASTER, http://aster.or.jp/business/contest/ doc/2015tdc-v1_1.zip, [14] ASTER: ASTER, http://aster.or.jp/business/contest/ doc/2015tdc-v1_1.zip, [15] ASTER, http://aster.or.jp/business/contest/ contest2015.html#agreement, [1] :,, (2008). [2] IPA/SEC:, https://www.ipa.go.jp/files/000026829.pdf, [3],, :,, Vol. 49, No. 7, pp.2304-2318, (2008). [4] VDM information web site, http://www.vdmtools.jp/, 8