2023.11.24
講座説明会

テストと検証シリーズご紹介
担当講師：

••
•
•
•
•

石川 冬樹 (NII)
宇佐美 雅紀 （Amazon Japan）
粂野 文洋 (日本工業大学)
久連石 圭 (東芝)
田辺 良則 (鶴見大学・NII)
長谷川哲夫 （東芝）

••
•
•
•
•

初谷 久史 （PRINCIPIA）
早水 公二 （フォーマルテック）藤本 洋 (イーソル)
前田 直人 (NEC)松崎 和賢 (中央大学)
吉岡 信和 （早稲田大学）

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

2

テストと検証シリーズ
ソフトウェアの品質確保に関する手法
n テスティング
n テスティング (基礎)n 静的解析
n プログラム解析

n モデル検査n モデル検査入門I, IIn 設計モデル検証
n モデル検査特論
n モデル検査事例演習
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

3

テストと検証シリーズ
ソフトウェアの品質確保に関する手法
n テスティング
n テスティング (基礎)n 静的解析
n プログラム解析

n モデル検査n モデル検査入門I, IIn 設計モデル検証
n モデル検査特論
n モデル検査事例演習
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

4テスティング (基礎)n テストツールn テスト駆動開発
n ブラックボックステストn 直交表n ホワイトボックステスト
n パスカバレッジ

n テスト自動化
n テスト計画n テストの管理と評価・改善
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

5

テストと検証シリーズ
ソフトウェアの品質確保に関する手法
n テスティング
n テスティング (基礎)n 静的解析
n プログラム解析

n モデル検査n モデル検査入門I, IIn 設計モデル検証
n モデル検査特論
n モデル検査事例演習
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

6プログラム解析n オムニバス形式で，いろいろな静的解析の手法・ツールを紹介する．
n 有界モデル検査 / CBMC
n データフロー解析 / SOBAn 記号実行 / Tritonn 契約による設計 / JML

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

7

テストと検証シリーズ
ソフトウェアの品質確保に関する手法
n テスティング
n テスティング (基礎)n 静的解析
n プログラム解析

n モデル検査n モデル検査入門I, IIn 設計モデル検証
n モデル検査特論
n モデル検査事例演習
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

8

モデル検査 : ターゲット
n 再現が難しい不具合
n 並行実行に起因するもの

n (例) 以下の条件が揃ったときだけ，ファイルをクローズしそこねる:n スレッド1 が メソッドa の20行目を実行したが，まだ21行目は実行していない
n スレッド2 が メソッドb の53行目を実行した

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

9モデル検査 : 考え方n システムが取り得るあらゆる状態を含む状態遷移系を構築する．
n 状態遷移系を効率よく探索して，不具合を起こす経路の有無を判断．
緑: スタート，黄色: オープン，赤: クローズ
オープンしたら必ずクローズされるか?
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

10モデル検査 : 考え方n システムが取り得るあらゆる状態を含む状態遷移系を構築する．
n 状態遷移系を効率よく探索して，不具合を起こす経路の有無を判断．
緑: スタート，黄色: オープン，赤: クローズ
オープンしたら必ずクローズされるか?
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

11モデル検査 : 学ぶ意義
n 並行実行に起因する，再現が難しい不具合を追求する手段を獲得できるn モデリング技術・抽象化技術の適用を学べる

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

12

モデル検査 : 手順成り立つべき性質

仕様書仕様書だけ?
ソースコードは?

オープンしたファイルは必ずクローズされる

性質ってどう書くの?

他の開発工程「OK」との関係は?
またはモデル検査が反例 (不具合に至る経路)
状態遷移系 (数学的モデル)有効な領域は?
時間制約も全数探索!
扱える? 網羅的遷移系のモデル作り方は?
検査結果を説検査器
明してわかってモデル検査器の 自動実行 もらえるかな?
使い方は?
: オープン: クローズ
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

13

性質ってどう書くの?

モデル検査入門I, II
n モデル検査の基礎理論

n 検証する性質の表現 = 時相論理
nLinear Temporal Logic
nComputational Tree Logicn 状態遷移系遷移系の作り方は?
モデル検査器の使い方は?

n 代表的なモデル検査器に習熟
n SMV - 状態遷移系を直接記述
n SPIN - プロセスをプログラミング言語風に記述

n ロボットを利用した実習
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

14

他の開発工程との関係は?

設計モデル検証
要求仕様

設計モデル

ソースコードUserDigitalTVDigitalTV

CellularPhone

public class Client extends Thread {public Object lock1;
public Object lock2;
public Client(Object lock1, Object lock2) {this.lock1 = lock1;
this.lock2 = lock2;}
public void run() {synchronized(lock1) {synchronized(lock2) {}}}Home NetworkDVDRecDVDRec設計

実装}

検証要求分析
検証モデル設計

設計誤り発見mtype DVD_recorder_state = waiting;

経験者の頭の中

active proctype HD_recorder() {mtype event;
do:: HD_ch?event ->if:: (HD_recorder_state == waiting && event == req_reserve_HD) ->HD_recorder_state = ready;DVD_ch!ack_reserve_HD:: (HD_recorder_state == ready && event == req_play_HD) ->progress1: HD_recorder_state = playing;
DVD_ch!ack_play_HD:: handle_playing_terminated_HD():: else -> skipfi:: handle_playing_terminated_HD()
od

実装

検証}

検証モデル

モデル検査記述

検証結果／反例

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

モデル検査特論 (その1)

モデル検査が有効な領域は?
モデル検査器FDRによる検証

プロセス代数CSP
によるモデル化

逐次システムや仕様

FDRスクリプト

CSPモデル
モデル化

並行システムや仕様

SRseq(K) = SendRec(0,0,0,K)
SendRec(n,m,i,K)= i<K & disp!send.n→ SendRec((n+1)%N,m,i+1,K) □i>0 & disp!receive.m→ SendRec(n,(m+1)%N,i-1,K)

FDR

並行システム実行
逐次システム

検証
検証項目

CSPモデルJCSPプログラム

SRconc= (Sender(0) [| {| chan |} |]Receiver(0))＼{| chan |}

モデル化

15

Sender(n)= disp!send.n → Sender'(n)Sender‘(n)= chan!n → Sender((n+1)%N)
Receiver(m)= chan?m → Receiver'(m)Receiver‘(m)= disp!receive.m → Receiver(m)Java

プロセス並行合成
Senderの動作

実装

実行

Receiverの動作

Javaライブラリ
JCSPによる実装

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

16

モデル検査特論 (その2)

時間制約も扱える?

n 組込みソフトウェアの時間制約に関する設計検証
n 講座で取り扱う課題n いろいろな時間要素の検証モデルへの反映方法と検証結果分析の難しさ
n 設計プロセスと検証プロセスのシームレスな連携

n 利用するツールn 時間制約を扱えるモデル検査ツールUPPAALnスウェーデンのUppsala大学とデンマークのAalborg
大学により開発

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

17

モデル検査事例演習【目的】企業におけるモデル検査推進者の育成
n モデル検査の実務（組織）を想定し，その開始から終了までの全プロセスを体験する演習【習得できる知識】
n 組織におけるモデル検査の適用プロセス
1.
2.
3.
4.
5.

開発者からのヒアリング
ソフトウェアのモデル化
モデル検査
結果報告
最終報告書

検査結果を説明してわかってもらえるかな?

n モデル検査報告書の作成方法
n モデル検査の導入を推進するためのノウハウ【検証対象】実例を基にしたソースコード (C言語)、もしくは仕様書
Copyright (C) 2023 National Institute of Informatics, All rights reserved.

18

科目間依存関係
テスティング基礎

プログラム解析
設計モデル検証
モデル検査入門II
モデル検査事例演習
モデル検査入門I

モデル検査特論

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

19

目的別科目選択例 -1ソフトウェア工学の基礎科目を幅広く受講したい
n テスティング基礎
n モデル検査入門I

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

20

目的別科目選択例 -2モデル検査技術をマスターしたい
n モデル検査入門I・II
n 設計モデル検証
n モデル検査特論
n モデル検査事例演習

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

21

目的別科目選択例 -3テスティング技術を基礎から応用まで学習したい
n テスティング基礎
n プログラム解析

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

22

目的別科目選択例 -4ソフトウェアの堅牢な構築についての技術全般に興味があり，マスターしたい
n テスティング基礎
n プログラム解析
n モデル検査入門I・II
n 設計モデル検証
n モデル検査特論
n モデル検査事例演習

Copyright (C) 2023 National Institute of Informatics, All rights reserved.

23[補足] モデル検査系科目群のまとめ
設計モデル検証では，UMLからの状態遷移系の作り方を学びます．開発プロセス中にモデル検査をどう組み込むかを検討します．

仕様書

UMLモデル事例

設計入門

時間Promela
オートマ
モデル
トンCSP
モデル特論

特論

モデル検査特論 では，時間制約をモデル検査する方法を学習します．

モデル検査器(all)

すべての講義で，モデル検査器を用いた実習を行います．

入門

状態遷移系
SMV
モデル

モデル検査入門では，基本的な状態遷移系と性質記述を学びます．

性質記述

モデル検査事例演習では，モデル検査の専門家と開発者の協働方法を検討します．仕様書からの状態遷移系作成も扱います．

検査結果
設計

事例

開発プロセス

モデル検査特論では，CSPモデルから状態遷移系を作りモデル検査し，同時に実装系も生成する手法を学習します．

Copyright (C) 2023 National Institute of Informatics, All rights reserved.