VDMの仕様記述言語を導入した状態遷移図とそのテスト基準の提案

全文

(1)情報処理学会第 80 回全国大会. 1B-03. VDM ࡢ௙ᵝグ㏙ゝㄒࢆᑟධࡋࡓ≧ែ㑄⛣ᅗ࡜ ࡑࡢࢸࢫࢺᇶ‽ࡢᥦ᱌ 㧗ᮌᬛᙪ† ㉥ᮌ❶⣖‡ 㤶ᕝ኱ᏛᕤᏛ㒊† 㤶ᕝ኱Ꮫ኱Ꮫ㝔ᕤᏛ◊✲⛉‡ . 1. ࡣࡌࡵ࡟ ኱つᶍ㸪」㞧࡞ࢯࣇࢺ࢙࢘࢔ࢆయ⣔ⓗ࡟ࢸࢫ ࢺࡍࡿࡓࡵࡢᢏ⾡ࡢࡦ࡜ࡘࡀ MBT㸦model-based testing㸧[1]࡛࠶ࡿ㸬MBT ࡛ࡣ㸪ࢸࢫࢺᑐ㇟ࢯࣇ ࢺ ࢘ ࢙ ࢔ ࡢ ᮇ ᚅ ࡉ ࢀ ࡿ ᣺ ⯙ ࠸ࢆᙧᘧⓗࣔࢹࣝ 㸦ᅗᘧࡸᙧᘧゝㄒ࡞࡝ࢆ⏝࠸࡚ࢥࣥࣆ࣮ࣗࢱࡀ ゎ㔘ᐇ⾜࡛ࡁࡿᙧᘧ࡛⾲⌧ࡉࢀࡓࣔࢹࣝ㸧࡟ࡼ ࡗ࡚ᐃ⩏ࡋ㸪ࡑࡢᙧᘧⓗࣔࢹࣝ࡟ᇶ࡙࠸࡚≉ᐃ ࡢࢸࢫࢺᇶ‽ࢆ‶ࡓࡍࢸࢫࢺࢣ࣮ࢫࢆ⏕ᡂࡍࡿ㸬 ᙧᘧⓗࣔࢹࣝࡣ㸪ᮇᚅࡉࢀࡿ᣺⯙࠸ࢆᢳ㇟໬ࡋ ࡘࡘ㸪ࢸࢫࢺࡉࢀࡿ࡭ࡁᮏ㉁ⓗ࡞ഃ㠃࡟ࡘ࠸࡚ ࡣ⢭ᐦ࡟⾲⌧࡛ࡁࡿᚲせࡀ࠶ࡿࡀ㸪୍⯡ⓗ࡟⏝ ࠸ࡽࢀ࡚࠸ࡿ≧ែ㑄⛣ᅗ࡛ࡣ༑ศ࡛ࡣ࡞࠸ሙྜ ࡀ࠶ࡿ㸬ࡓ࡜࠼ࡤ㸪࢔ࢡࢩࣙࣥ㸦㑄⛣࡟௜㝶ࡍ ࡿࢯࣇࢺ࢙࢘࢔ࡢᵝࠎ࡞᣺⯙࠸㸧ࡸ࣮࢞ࢻ㸦㑄 ⛣ࡀⓎⅆࡍࡿࡓࡵࡢ᮲௳㸧ࢆᙧᘧⓗ࡟⾲⌧ࡍࡿ ᪉ἲࡣᚲࡎࡋࡶ⤫୍ࡉࢀ࡚࠸࡞࠸㸬 ᮏ✏࡛ࡣࡲࡎ㸪࢔ࢡࢩࣙࣥࡸ࣮࢞ࢻࡶྵࡵ࡚ ᙧ ᘧ ⓗ ࡟ グ㏙ ࡍ ࡿ ࡓ ࡵ ࡟ 㸪 VDM 㸦 Vienna development method㸧[2]࡛౑⏝ࡉࢀࡿ௙ᵝグ㏙ゝㄒࢆᑟධࡋࡓ≧ែ㑄⛣ᅗࢆᥦ᱌ࡍࡿ㸬ᮏ✏࡛ࡣ ࡇࢀࢆᣑᙇ≧ែ㑄⛣ᅗ࡜࿧ࡪࡇ࡜࡜ࡍࡿ㸬ࡉࡽ ࡟㸪ࢸࢫࢺᇶ‽ࡣᙧᘧⓗࣔࢹࣝ࡜ᐦ᥋࡞㛵ಀ࡟ ࠶ࡿࡢ࡛㸪ᣑᙇ≧ែ㑄⛣ᅗ࡟ᇶ࡙࠸࡚య⣔ⓗ࡟ ࢸࢫࢺࢣ࣮ࢫࢆ⏕ᡂࡍࡿࡓࡵࡢࢸࢫࢺᇶ‽࡟ࡘ ࠸࡚ࡶᥦ᱌ࡍࡿ㸬. 2. ᣑᙇ≧ែ㑄⛣ᅗ ᣑᙇ≧ែ㑄⛣ᅗࡣ㸪ࢸࢫࢺᑐ㇟ࢯࣇࢺ࢙࢘࢔ ඲యࡲࡓࡣࡑࡢᵓᡂせ⣲㸦௨㝆㸪ࣔࢹࣜࣥࢢᑐ ㇟࡜࿧ࡪ㸧ࡢᢳ㇟໬ࡉࢀࡓ᣺⯙࠸ࢆᙧᘧⓗ࡟グ㏙ࡍࡿࡓࡵࡢ⾲グἲ࡛࠶ࡿ㸬ᅗ 1 ࡟ᣑᙇ≧ែ㑄 ⛣ᅗࡢ౛ࢆ♧ࡍ㸬ᣑᙇ≧ែ㑄⛣ᅗࡢ୺せ࡞ᵓᡂ せ⣲ࡣ㸪≧ែ㸦ࣀ࣮ࢻ㸧࡜㑄⛣㸦࢔࣮ࢡ㸧࡛࠶ ࡿ㸬≧ែࡣ㸪ཷ⌮ྍ⬟࡞࢖࣋ࣥࢺࡢ㞟ྜ࡟ࡼࡗ ࡚≉ᚩ௜ࡅࡽࢀࡿ㸬ࡓ࡜࠼ࡤᅗ 1 ࡣ㸪3 ✀㢮ࡢ࢖ ࣋ࣥࢺࡢཷ⌮ྍ⬟ᛶ࡟ࡼࡗ࡚≉ᚩ௜ࡅࡽࢀࡿ 3 State transition diagram using a VDM specification description language and its test criteria † Tomohiko Takagi ࣭ Faculty of Engineering, Kagawa University, Takamatsu, Kagawa 761-0396, Japan ‡ Akinori Akagi࣭Graduate School of Engineering, Kagawa University, Takamatsu, Kagawa 761-0396, Japan. instance variables public v : nat := 0; event_c( ) / v:=0;. state_1. event_a( ) [v>0]. state_2. event_b(nat p) / v:=v+p;. state_3. event_a( ). event_c( ) [v mod 2=1] (A) / v:=v+1; event_b(nat p) [v mod 2=0] / if v=p then v:=0 else v:=p; . . ᅗ 1. ᣑᙇ≧ែ㑄⛣ᅗࡢ౛ ࡘࡢ≧ែ࠿ࡽᵓᡂࡉࢀࡿ㸬࢖࣋ࣥࢺࡣࣔࢹࣜࣥ ࢢᑐ㇟࡟ᑐࡍࡿධຊ࡛࠶ࡾ㸪㑄⛣ࡢࢺࣜ࢞࡜࡞ ࡿ㸬㑄⛣ࡣ㸪࣮࢞ࢻ㸪ᘬᩘ㸪࢔ࢡࢩࣙࣥࢆక࠺ ࡇ࡜ࡀ࡛ࡁࡿ㸬࣮࢞ࢻࢆ‶ࡓࡉ࡞ࡅࢀࡤ㑄⛣ࡣ Ⓨⅆ࡛ࡁ࡞࠸㸬ࡓ࡜࠼ࡤᅗ 1 ࡢ(A)ࡢ㑄⛣ࡣ㸪⌧ ᅾࡢ≧ែࡀ state_3 ࡛࠶ࡾ㸪࢖ࣥࢫࢱࣥࢫኚᩘ v ࡀഅᩘࡢሙྜ࡟㝈ࡾ㸪event_b ࡢ⏕㉳࡟ࡼࡗ࡚Ⓨ ⅆ࡛ࡁࡿ㸬࡞࠾㸪࢖ࣥࢫࢱࣥࢫኚᩘࡣ㸪ࣔࢹࣜ ࣥࢢᑐ㇟ࡢ᣺⯙࠸ࢆ≉ᚩ௜ࡅࡿ୺せ࡞ኚᩘ࡛࠶ ࡿ㸬ᘬᩘࡣ㸪ࣔࢹࣜࣥࢢᑐ㇟࡟ᑐࡍࡿ୺せ࡞ධ ຊࢹ࣮ࢱ࡛࠶ࡾ㸪ᙜヱ㑄⛣࡟௜㝶ࡍࡿ࢔ࢡࢩࣙ ࣥෆ࡛౑⏝ࡉࢀࡿ㸬࢔ࢡࢩࣙࣥࡣᙜヱ㑄⛣ࡢⓎ ⅆ᫬࡟ᐇ⾜ࡉࢀ㸪࢖ࣥࢫࢱࣥࢫኚᩘࡢ᭦᪂ࢆࡶ ࡓࡽࡍ㸬ࡓ࡜࠼ࡤ㸪ᅗ 1 ࡢ(A)ࡢ㑄⛣࡟క࠺ nat ᆺᘬᩘ p ࡣ㸪ᙜヱ㑄⛣ࡢ࢔ࢡࢩࣙࣥෆ࡛࢖ࣥࢫ ࢱࣥࢫኚᩘ v ࢆ᭦᪂ࡍࡿࡓࡵ࡟౑⏝ࡉࢀࡿ㸬 ᣑᙇ≧ែ㑄⛣ᅗୖࡢ⤒㊰㸦㛤ጞ≧ែ࠿ࡽጞࡲ ࡿ≧ែ㑄⛣ิ㸧ࡀࣔࢹࣜࣥࢢᑐ㇟ࡢᮇᚅࡉࢀࡿ ᐇ⾜㐣⛬࡛࠶ࡾ㸪ࢸࢫࢺࢣ࣮ࢫ࡜࡞ࡿ㸬 ᡃࠎࡣ[3]࡟࠾࠸࡚ࣉ࣮ࣞࢫ/ࢺࣛࣥࢪࢩࣙࣥࢿ ࢵࢺ࠿ࡽ VDM ௙ᵝࢆᵓ⠏ࡍࡿᡭἲࢆᥦ᱌ࡋࡓ㸬 ࡇࢀ࡜ྠᵝ࡟㸪୍⯡ⓗ࡞ VDM ⏝ࢶ࣮ࣝࢆ⏝࠸࡚ ᐇ⾜ࡸศᯒࢆ⾜࠺ࡓࡵ࡟㸪ᣑᙇ≧ែ㑄⛣ᅗ࠿ࡽ VDM ௙ᵝࢆᶵᲔⓗ࡟ᵓ⠏ࡍࡿࡇ࡜ࡀ࡛ࡁࡿ㸬ᅗ 1 ࡢᣑᙇ≧ែ㑄⛣ᅗࢆ VDM ௙ᵝ㸦VDM++ࡢࢥ ࣮ࢻ㸧࡟ኚ᥮ࡋࡓ୍౛ࢆᅗ 2 ࡟♧ࡍ㸬. 1-173. Copyright 2018 Information Processing Society of Japan. All Rights Reserved..

(2) 情報処理学会第 80 回全国大会. FODVV67' W\SHVᆺᐃ⩏ SXEOLF6WDWH VWDWHB!_VWDWHB!_VWDWHB! LQVWDQFHYDULDEOHV࢖ࣥࢫࢱࣥࢫኚᩘᐃ⩏ SXEOLFFXUBVWDWH 6WDWH VWDWHB! SXEOLFYQDW . (1) (2) (3) (4) (5) (6) (7). ⌧ᅾࡢ≧ែࢆ ಖᣢࡍࡿኚᩘ ࢔ࢡࢩࣙࣥࡸ࣮࢞ࢻ ࡛౑⏝ࡍࡿኚᩘ. RSHUDWLRQV᧯సᐃ⩏ SXEOLFHYHQWBD

(3) !ERRO HYHQWBD

(4) ͐୰␎͐

(5) SXEOLFHYHQWBEQDW !ERRO HYHQWBE S

(6) LIFXUBVWDWH VWDWHB! WKHQ Y YS FXUBVWDWH VWDWHB!UHWXUQWUXH

(7) HOVHLIFXUBVWDWH VWDWHB!DQGYPRG WKHQ LIY SWKHQY HOVHY S FXUBVWDWH VWDWHB!UHWXUQWUXH

(8) UHWXUQIDOVH

(9) SXEOLFHYHQWBF

(10) !ERRO HYHQWBF

(11) ͐୰␎͐

(12) HQG67'. HYHQWBD࡟ ࡼࡿ᣺⯙࠸. state_1 → event_a → state_2 state_1 → event_b / v:=v+p; → state_3 state_2 → event_a → state_3 state_2 → event_c / v:=0; → state_1 state_3 → event_b / v:=0; → state_1 state_3 → event_b / v:=p; → state_1 state_3 → event_c / v:=v+1; → state_2 . . ᅗ 3. ᣑᙇ 0 ࢫ࢖ࢵࢳ⥙⨶ᇶ‽ࡢ ᐃᑐ㇟ ࢀࡓሙྜ㸪ᣑᙇ 0 ࢫ࢖ࢵࢳ⥙⨶⋡ࡣ⣙ 28.6㸣㸦2/7㸧࡜࡞ࡿ㸬 . HYHQWBE࡟ ࡼࡿ᣺⯙࠸. 4. ࠾ࢃࡾ࡟ HYHQWBF࡟ ࡼࡿ᣺⯙࠸. . . ᅗ 2. VDM ௙ᵝ࡬ࡢኚ᥮ࡢ୍౛. 3. ᣑᙇ≧ែ㑄⛣ᅗࡢࡓࡵࡢࢸࢫࢺᇶ‽ ࢸࢫࢺᇶ‽ࡣࢸࢫࢺ඘ศᛶࢆホ౯ࡍࡿࡓࡵࡢ ࡶࡢ࡛㸪 ᐃᑐ㇟࡟ࡼࡗ࡚ᐃ⩏ࡉࢀࡿ㸬 ᐃᑐ ㇟ࡣ㸪ᙜヱࢸࢫࢺᇶ‽ࢆ‶ࡓࡍࡓࡵ࡟ࢸࢫࢺࡉ ࢀࡿᚲせࡢ࠶ࡿ㡯┠࡛࠶ࡾ㸪඲㡯┠ᩘ࡟ᑐࡍࡿ ࢸࢫࢺ῭ࡳ㡯┠ᩘࡢ๭ྜࢆ⥙⨶⋡࡜࠸࠺㸬≧ែ 㑄⛣ᅗࡢࡓࡵࡢ୍⯡ⓗ࡞ࢸࢫࢺᇶ‽࡜ࡋ࡚ࡣ㸪 ≧ែ⥙⨶ࡸ㑄⛣⥙⨶㸪N ࢫ࢖ࢵࢳ⥙⨶࡞࡝ࡀ▱ ࡽࢀ࡚࠸ࡿ㸬ࡇࢀࡽࡣ≧ែ㑄⛣ᅗࡢࣀ࣮ࢻࡸ࢔ ࣮ࢡ㸪ࡲࡓࡣࡑࡢ⤌ྜࡏࢆ ᐃᑐ㇟࡜ࡋ࡚⪃៖ ࡋࡓࡶࡢ࡛࠶ࡿࡀ㸪୍᪉㸪ᣑᙇ≧ែ㑄⛣ᅗ࡛ࡣ ࢔ࢡࢩࣙࣥ࡞࡝ࢆᵓᡂࡍࡿࢥ࣮ࢻ࡟ࡘ࠸࡚ࡶ⪃ ៖ࡍࡿᚲせࡀ࠶ࡿ㸬ࡑࡇ࡛ᮏ◊✲࡛ࡣ N ࢫ࢖ࢵ ࢳ⥙⨶ࢆᣑᙇࡋࡓ᪂ࡓ࡞ࢸࢫࢺᇶ‽㸦ᣑᙇ N ࢫ ࢖ࢵࢳ⥙⨶ᇶ‽㸧ࢆᥦ᱌ࡍࡿ㸬 ᣑᙇ N ࢫ࢖ࢵࢳ⥙⨶ᇶ‽ࡢ ᐃᑐ㇟ࡣ㸪ᚑ᮶ ࡢ N ࢫ࢖ࢵࢳ⥙⨶ᇶ‽࡜ྠᵝ㸪ᐇ⾜ྍ⬟࡞㛗ࡉ N+1 ࡢ㐃⥆ࡍࡿ≧ែ㑄⛣ิ࡛࠶ࡿࡀ㸪ᐇ⾜ࡉࢀ ࡿ࢔ࢡࢩࣙࣥࡢࢥ࣮ࢻࡢ㞟ྜ࡟ࡼࡗ࡚≧ែ㑄⛣ ิࡀ༊ูࡉࢀࡿ㸬ᅗ 1 ࡟ᑐࡋ࡚ᣑᙇ 0 ࢫ࢖ࢵࢳ ⥙⨶ᇶ‽ࢆ㐺⏝ࡋࡓሙྜࡢ ᐃᑐ㇟ࡢࣜࢫࢺࢆ ᅗ 3 ࡟♧ࡍ㸬(A)ࡢ㑄⛣ࡢ࢔ࢡࢩࣙࣥෆ࡟ if ᩥࡀ Ꮡᅾࡋ㸪ࡑࡢ᮲௳ᘧ v=p ࡢุᐃ⤖ᯝ࡟ࡼࡗ࡚ᐇ ⾜ࡉࢀࡿࢥ࣮ࢻࡀ␗࡞ࡗ࡚ࡃࡿࡓࡵ㸪ᚑ᮶ࡢ 0 ࢫ࢖ࢵࢳ⥙⨶ᇶ‽࡛ࡣ 1 ࡘࡢ ᐃᑐ㇟࡜ࡋ࡚ᢅ ࢃࢀࡿ㛗ࡉ 1 ࡢ≧ែ㑄⛣ิࠕstate_3 Ѝ event_b Ѝ state_1ࠖࡀ㸪ᅗ 3 ࡢ(5)࡜(6)࡟ศ๭ࡉࢀࡿ㸬 ࡓ࡜࠼ࡤ㸪ࢸࢫࢺࢣ࣮ࢫࠕstate_1 Ѝ event_b(6) / v:=0+6; Ѝ state_3 Ѝ event_b(10) / v:=10; Ѝ state_1ࠖࡀᅗ 1 ࡢࣔࢹࣜࣥࢢᑐ㇟࡟ᑐࡋ࡚ᐇ⾜ࡉ. VDM ࡢ௙ᵝグ㏙ゝㄒࢆᑟධࡋࡓ≧ែ㑄⛣ᅗ 㸦 ᣑ ᙇ ≧ ែ 㑄 ⛣ ᅗ 㸧㸪 ࠾ ࡼ ࡧࡑࡢࢸࢫࢺᇶ‽ 㸦ᣑᙇ N ࢫ࢖ࢵࢳ⥙⨶ᇶ‽㸧ࢆᥦ᱌ࡋࡓ㸬ᮏ✏ ࡛ࡣ㸪༢୍ࡢᣑᙇ≧ែ㑄⛣ᅗ࡟ࡼࡿ౛࡟ᇶ࡙࠸ ࡚㆟ㄽࡋࡓࡀ㸪」ᩘࡢᣑᙇ≧ែ㑄⛣ᅗࢆ⏝࠸࡚ ࣔࢹࣜࣥࢢᑐ㇟ࡢ᣺⯙࠸ࢆᐃ⩏ࡍࡿࡇ࡜ࡶྍ⬟ ࡛࠶ࡿ㸬ࡑࡢሙྜࡣ㸪ࢸࢫࢺᇶ‽ࢆ‶ࡓࡍࡓࡵ ࡟ከࡃࡢࢸࢫࢺࢣ࣮ࢫࡀᚲせ࡜࡞ࡿሙྜࡀ࠶ࡿ ࡢ࡛㸪ࡓ࡜࠼ࡤ㸪 ᐃᑐ㇟࡟㔜ࡳࢆ௜୚ࡍࡿ࡞ ࡝㸪⌧ᐇࡢ㝈ࡽࢀࡓ࢚ࣇ࢛࣮ࢺ࡛ࡶᐇ⾜࡛ࡁࡿ ࡼ࠺ࢸࢫࢺࢣ࣮ࢫࡢඃඛ㡰఩௜ࡅࢆ⾜࠺௙⤌ࡳ ࡀᚲせ࡛࠶ࡿ㸬ࡲࡓ㸪ᮏ✏ࡢࢸࢫࢺᇶ‽࡛ࡣ࢔ ࢡࢩࣙࣥෆࡢᐇ⾜ࡉࢀࡓࢥ࣮ࢻࡢ㞟ྜࢆ⪃៖ࡋ ࡚࠸ࡿࡀ㸪ࡉࡽ࡟⦓ᐦ࡞ࢸࢫࢺࢆྍ⬟࡜ࡍࡿࡓ ࡵ࡟㸪ࡓ࡜࠼ࡤ㸪」ྜ᮲௳ᘧࢆᵓᡂࡍࡿྛ᮲௳ ᘧࡢ┿ഇࡢ⤌ྜࡏࢆ⪃៖ࡋࡓࡾ㸪࢖ࣥࢫࢱࣥࢫ ኚᩘࡢᐃ⩏࡜ཧ↷ࡢ㛵ಀࢆ⪃៖ࡋࡓࡾࡍࡿ࡞࡝㸪 ୖ఩ࡢࢸࢫࢺᇶ‽ࢆ㛤Ⓨࡍࡿࡇ࡜ࡶ⪃࠼ࡽࢀࡿ㸬 ௒ᚋࡣ㸪ୖ㏙ࡢㄢ㢟࡟ྲྀࡾ⤌ࡴ࡜࡜ࡶ࡟㸪ࢸ ࢫࢺᇶ‽ࢆ‶ࡓࡍࢸࢫࢺࢣ࣮ࢫࢆ⏕ᡂࡍࡿࡓࡵ ࡢࢶ࣮ࣝࢆᵓ⠏ࡋ㸪ホ౯ࢆ⾜࠺ணᐃ࡛࠶ࡿ㸬 . ㅰ㎡ ᮏ◊✲䛿㻶㻿㻼㻿 ⛉◊㈝㻶㻼㻝㻣㻷㻜㻜㻝㻜㻟䛾ຓᡂ䜢ཷ䛡䛯䠊㻌 . ཧ⪃ᩥ⊩ [1] M. Utting, A. Pretschner, B. Legeard, "A taxonomy of model-based testing approaches", Software Testing, Verification and Reliability, Vol.22, pp.297-312, 2012. [2] J. Fitzgerald, P.G. Larsen, P. Mukherjee, N. Plat, M. Verhoef, Validated Designs for ObjectOriented Systems, Springer-Verlag London, 2005. [3] 㧗ᮌᬛᙪ, ㉥ᮌ❶⣖, "ᣑᙇࣉ࣮ࣞࢫ/ࢺࣛࣥࢪ ࢩࣙࣥࢿࢵࢺ࡟ᇶ࡙ࡃ VDM ௙ᵝࡢᵓ⠏ᡭἲ ࡢ ᥦ ᱌ ", ᝟ ሗ ฎ ⌮ Ꮫ ఍ ➨ 79 ᅇ඲ᅜ኱఍, pp.195-196, 2017.. 1-174. Copyright 2018 Information Processing Society of Japan. All Rights Reserved..

(13)