================================================================================
8/26 13:20〜15:00
チュートリアル２
セッションS2-3-1:「モデル検査ツールSpinによる組込みソフトウェアの検証」

講師: 青木 利晃（北陸先端科学技術大学院大学）

席数　：約30席
参加者：約20名
================================================================================
モデル検証がいろいろいわれているが、モデル検査ツールであるSpinを紹介する。
また、組込みソフトウェアにどう使われているか説明する。

・ソフトウェアの信頼性
    現在、社会システムの様々な場所にソフトウェアが組み込まれている。
        -バンキングシステム、航空管制、携帯電話など
    これらの中には、誤りを含むものが少なくないのが現状。
    正しいソフトウェアを作ることが重要である。
    ソフトウェアの信頼性を高めるため、現在はテスト手法の開発が中心。
    しかし、ソフトウェアの規模の拡大により、テスト手法では時間やコストがかかって
    しまう。
    テスト手法から取って代わるものとして、形式的手法／検証がある。

・テストと検証
テスト…限られた実行列（テストケース）で誤りが無いことを保障する。
        実行列は無限にあるので重要なトコだけテスト
　　　　テストされてない部分は正しいのか？
検証　…組み合わせが無限にあるなかでどうやって正しいことを保障するか？
　　　　→数学的、論理的基盤に基づいて正しさを証明する

・ソフトウェアの検証
    検証する対象はプログラムだけじゃなく、様々なものがある。
        仕様書、設計書、プログラムなど
    プログラムのチェックだけでは効果が薄い。
    仕様、設計を厳密に書いて、チェックすることが大切。
        仕様、設計をプログラムのように実行可能な言語で書いてみる
    仕様、設計記述言語
        ＵＭＬ：クラス図、ステートチャートなど
    昔はソフトウェア検証検証技法が数多く存在したが、最近では２つがメイン。
    ・モデル検査技法（Spinもその１つ）
        しらみつぶし、自動的
    ・定理証明技法
        述語論理、推論規則、人間の介入が必要

・簡単な例
    職場にプリンタとスキャナが１台づつ。ＡさんとＢさんが仕事をする例を紹介。
    ４つの状態遷移図を、まず１つの状態遷移図にする。
    →１つにまとめることがはじめの一歩

・モデル検査ツールSPIN
    SPINとは
        AT&T Bell研が開発したモデル検査ツール。
      　1980年代に開発され、現在も継続的にバージョンアップされている。
  　チャネル通信オートマトンのためのモデル検査ツール
        並行動作する有限オートマトン。
        オートマトン同士はチャネルを使って通信を行う。
    Promela:チャネル通信オートマトンを記述するための言語
        SPINはPromelaによる記述を入力として、網羅的に状態を探索し、
        その性質を検査する。
    ※Promela記述の紹介と説明（上記にある、簡単な例を記述）

--------------------------------------------------------------------------------
質問：Promelaで書いたものは状態遷移図と同等であるが、ＳＤＬとどう違うのか？
回答：ＳＤＬには派生がある。
質問：設計用にも使うことが出来るのか？
回答：設計も出来るし、検証もできる。
--------------------------------------------------------------------------------

    SPINによる実行
        Promelaによる記述はシミュレーション実行することが出来る。
    SPINによるモデル検査
        pan(Protocol ANalyzer)を自動生成する
            状態を網羅的に探索してくれる実行形式ができる。
            状態遷移図を作ってくれる。
    ※端末上でSpinのプログラムを作成し、コンパイルして実行デモを行った。
      検査結果を表示し、正常でない性質が検出された場合に、それを導く例を出力。
      DeadLockが起こる例も紹介。
      
・モデル検査のプロセス
    ※モデル検査のフローチャートを紹介
    
・様々な性質の検証
    Spinにより検査できること
        ・表明
        ・到達性
        ・進行性
        ・性質オートマトン
        ・LTL式

・進行性調査
頻繁に訪れるポイントにラベルを付ける
    ※ラベルを用いたモデル検査のデモの紹介
      プログラムのコンパイルと実行
    　デモ結果→ラベルの場所に訪れないような無限の実行列が存在します
      反例も紹介

・反例
    反例が意味すること
        上記の簡単な例において、PersonBばかりがずっとPrinterとScannerを
        使う状況がある。
    飢餓状態(Starvation)
        資源が枯渇していて、獲得できない状況。
            PersonBが資源を食い尽くして、PersonAが資源を獲得できない状況に
            なっている。

・進行性検査
    解決策を模索してみる
        ・ＡさんとＢさんの実行を交互に行ってはみてはどうか？
        ※実際にプログラムを書き換えてデモを実行
--------------------------------------------------------------------------------
質問：この修正したプログラムでもＢさんが飢餓状態にならないか？
回答：デモで確認してみましょう→起きませんでした
　　　※シミュレーション実行（実行系列の表示）もやってみる
質問：交互に実行させることできないとすると、Ａさんが連続して
　　　仕事をしたいときにもＢさんに仕事が行ってしまって効率が
　　　悪いのでは？（排他制御を導入すると良いのでは？）
回答：ＬＴＬで解決できる（後で説明します）
--------------------------------------------------------------------------------
・時相論理
    述語論理や命題論理では時間について（直接的に）言及できない。
    線形時相論理（Liner Temporal Logic)
        述語論理や命題論理に時間の概念を入れた（今回は命題論理に入れた）もの
    通常の論理式に、時間を表現する演算子を用いる。

・様相演算子
    各種の時間を表現する演算子を説明。
        ダイヤマーク　…いつかはＴになる（どこか一箇所がＴになる）時間がある
        四角マーク　　…ずーっとこの先Ｔのとき、成立
        Ｘ　　　　　　…現在から次の時間に移ったときにＴになるとき成り立つ
        p∪q　　　　　…qがＴになるまでpがＴである

・ＬＴＬ式の検査
    排他制御の記述例
    Promelaで記述したモデルの性質をLTL式で記述し、SPINでチェックする
    ※LTL式をチェックするデモ
--------------------------------------------------------------------------------
質問：排他制御などのパターンをまとめたもの（文献）がある？
回答：ない。現状はノウハウを蓄積することが重要。
--------------------------------------------------------------------------------
・組み込みシステムへの応用
    組込みソフトウェアに出てきそうなものを検証してみる
        Sleep/Wakeup、Semaphore、優先度などの概念
    Promelaには、それらの概念は無い
    いくつかの概念について、Spinによる検査法を紹介

・Mutex（ロック・アンロック）
    共有資源を予約する操作による排他制御の実現方法の1つである、Mutexを紹介
        Mutex
        ・状態‐ロック状態、アンロック状態
        ・操作‐ロック、アンロック
    ※Mutexを用いたプロセス制御のソースを紹介＆デモ
    変数の競合も検査可能

・Sleep/Wakeup
    プロセスの実効制御を行うことが出来る
        Sleep/Wakeupを用いて、生産者‐消費者問題を記述
    ※生産者‐消費者問題のソースを記述、コンパイル、実行のデモ。
      デッドロックが起こる反例を紹介
    モデル検査の難しさは反例の読み方、きっちりログを読んでいくしかない

・セマフォ
    複数個の資源に対応
    Mutexはセマフォの機能を限定したもの
    セマフォで生産者‐消費者問題を解決することができる
    ※セマフォを用いて、生産者‐消費者問題を解決するPromela記述の紹介
      コンパイル、実行を行い、反例が出ないことを確認。
      バッファ溢れと、バッファにデータが無いときにアクセスしないことを検査

---その他の話題
Plomeraを用いて、RTOS（μITRON）のAPIをベースとした検証を行えるようにした。
ある程度まとまったら公開予定とのこと。

・様々なモデル検査ツール１
    他にもいろいろあるモデル検査ツールの紹介
        時間オートマトンや、ハイブリットオートマトンなど
・使用例
    モデル検査ツールの使用例を紹介
        ネットワークサーバ＋交換機　…　Promela/SPINなど

・おわりに
    モデル検査
        決して難しくない。
        研究領域から実践領域へ活用されることを願っている。
            書けることと実際の製品に適用できることは別。
        日常的に開発で使って欲しい。
    ノウハウの蓄積とソフトウェア工学の観点からの整理が必要
--------------------------------------------------------------------------------   
質問：PlomeraからCに変換してるのはなにしてる？
回答：変換されたC言語は状態遷移図を記述する文を作っているだけ。
--------------------------------------------------------------------------------   
--------------------------------------------------------------------------------   
質問：ＨＷのタイマで扱うような実時間を扱うことができる？
回答：難しい。カウンタを入れるとそれだけ状態数が増えてしまう。
--------------------------------------------------------------------------------