7/23 チュートリアル　セッションSC-6 「組み込みシステム開発への形式的手法の適用」 独立行政法人産業技術総合研究所システム検証研究センター 　　木下佳樹 　　水口大知 会場は93座席で35人程度が参加 ------------------------------------------------------------------------------ 木下氏　: この講演の前半では形式的手法の考え方を、後半ではモデル検査について説明する。 形式的手法、英語ではFormal methodというが、これは何であるのだろうか。 形式という言葉は、二通りの意味に使われる。”数学的に”という意味と、”マシン処 理可能な”という意味である。 形式論理とは何だろうか。 数理モデルを考え、自然言語を超える公理などをきっちりさせる。これで、記号言語、 そして整式的言語が出来上がる。数理的モデルをつくるのが大事なのである。 どのように数理モデルを立てるか。 ソフトウェアか組み込みシステムかは関係ない。大事なのは入力出力型か刺激応答型の 区別である。また、実時間は考えない。 入力出力型とは、入力データを受け、入力処理と計算をし、出力する。このとき、過程 は考えない。数学的には写像といえる。刺激応答型とは、刺激に相当するデータを受け、 応答する。これを繰り返す。これは、無限ループである。数学的には遷移系である。 刺激応答型は刺激の無限列を受け、応答の無限列を考えられるが、データは有限のもの と考えたい。 入力出力型はループしてはいけない。刺激応答型はループする。停止してはいけない。 入力出力型は写像、刺激反応型は遷移系であり、強力である。 そのため、いろいろなところで使われている。それに対し、タイムドオートマトンはコ ンピュータでしか使われない。 この講演では、刺激応答型に焦点をしぼる。 システムの仕様を数学的に記述し、仕様を満たすことを証明する。 組み込みシステムは刺激応答型である。したがって、刺激応答型に焦点をあてる。 どんな性質を検証すればよいだろうか。 よく使う形の性質に対象を制限する。刺激応答型の大事な性質は、安全性と活性である。 安全性とは、現在も未来永劫に渡り悪いことが起きない性質のことである。 活性とは、常に、ある条件が満たされればいい事が必ず起こる。いつでも次のチャンス があるという性質のことである。 数理的技法の作り方、どうやって検証するかを説明する。 数理的技法はシステムの正しさの保証ではなく、バグを検出するものである。 数理的技法は、コードレビューをソフトウェアで可能にする。 テストとコードレビューについて触れる。 テストは実記を稼動させ、動作を観察する。全体を行う必要があり、ハードウェアかシミ ュレータが必要になる。全数テストは不可能である。コードレビューは、人間がソースコ ードを読み直す。 数理的技法のシナリオ。 モデル化として、数学の世界へ持っていく。これで、要求する項目をはっきりさせる。 次に、形式的、記号言語へ持っていき、公理系をはっきりさせる。 システムの一検証項目満たすか調べる。満たさなかった場合、バグかどうかを検討、判断 する。これは、開発者が行う。満たした場合、バグは見つからなかったといえるが、バグ がないとは言い切れない。 モデル化、形式化が正しいかを検証する。 形式論理の中での検証を計算機で支援できる。これは、形式化の利益である。 しかし、中には自動検証が不可能な体系がある。無数にあるものを扱う体系がそれである。 定理証明支援系は、人間が書き、計算機でチェックできるようにする基本は人間が行う。 XORなのか、ANDなのか、いろいろな方式がある。 いろいろなプログラム言語があるようなものである。検証の場合は、複数の方式を選べる。 これは、ANDの選択といえる。プログラム言語の場合は、一つしか選べないXORの選択であ る。 刺激応答型のための論理。 論理は山ほどあるが、どれが正しい論理式なのかが決まればよい。最も基本的なのは命題 論理であり、推論規則は三段論法である。命題変数に真偽を割り当て、論理式に対して真 偽を決める。一階論理では、データしか動かない。高階論理では、数学的帰納法のような 事が実現できる。 大切なのは様相である。刺激応答型の動的な振る舞いを書くのに便利である。 背景に遷移系があり状態により真偽が変わる。様相論理は、1ステップ後しか考えられない が、安全性は後をすべて考えるので、不動点を用いる。 CTLやLTLは様相μ計算の部分系である。実際にはこれらが用いられる。 数理的技法は、開発現場に有効かどうかだが、現在、指標が考えれている。 リスク管理も必要だが、必ずしも数理的技法とは結び付けられていない。 最後に、CVSの活動にはフィールドワークがあるが、数理的技法は 有効に用いられている。フィールドワークでは、パートナーからの信頼が大切である。 また、開発現場の人からの推進者も大切である。 また、研修コースも進めているコンソーシアム「システム設計検証技術研究会」も 作っている。研修会も開いている。 ------------------------------------------------------------------------------ 水口氏　: この講演の内容は、モデル検査の組み込みシステムへの適用事例紹介である。途中、 モデル検査ツールの使い方を紹介する。 フィールドワークでは、組み込み機器のソフトウェア仕様書にモデル検査を適用した。 その結果、仕様書の不備を発見できた。特徴として、ソフトウェア技術者が集まって、 モデル検査ツールを使用して、開発中の組み込みソフトウェア仕様書を検査したことが ある。 では、検査対象はどうだろうか。作業手順はどうだろうか。 コーディング直前のプログラム仕様書を検査する。メイン処理と割り込み処理によって 構成される組み込み機器で、OSはなく、多重割り込みもない。 主な4つの機能X,Y,Z,Wを検査した。Xモジュールはタイマのタイムアウトで起動す る。これは、外部信号からモジュールを動かすが、その外部信号の正常・異常を見る。 Yは、Xにメイン処理を組み合わせたもので、CPUを制御する。 Z,Wは複雑なので割愛する。 プログラム仕様が機能仕様を実現している事を検査する。 今回は、外部信号の異常が続いたらシステムを停止、システムが停止中なら、CPUはある 状態、外部信号が正常に戻ったらシステム再開する事を検査する。 あらゆる状況において、検査項目が真であるか否かをモデル検査ツールにより検査する。 機能Yを検査例を挙げる。 検査項目は、システムの動作が中断状態にあるとき、CPUは状態Qであること。ツールで 検査した結果、Falseであった。システムの動作が中断状態にあるとき、CPUは状態Qで ないことがある、という反例があった。 反例を解析すると、原因はモジュールDの実行中に設計者が意図しないタイミングでタイ マβによる割り込みが発生する事があることだった。 作業手順は、仕様書を作成し、モデルを作成する。これに並行し、検査項目を作る。 そして、ツールに入れると結果が得られるので、仕様書にフィードバックする。 まずは、小さな機能αを考える。これは、メイン処理と割り込みから成る。メイン処理は、 開始後i:=0, m:=0とし、iが0ならばm:=0, iが1ならばm:=1とするループに入るものである。 割り込みがあると、iを否定、つまりiが0ならiを1とし、iが1ならiを0にする。 これをモデル検査する。 モデル検査機UPPAALでは、モデルを時間オートマトンの集まりとし、検査式をCTLの一部 とし、これを用いる。 機能αをモデル化すると、5つのオートマトンになる。この5つがバラバラに動くが、同期 して遷移する部分もある。 メイン処理はそのまま表現される。ただし、tickと同期して遷移する。 次のようなモデルを考える。時計変数xがあり、xが1のときtickしてxをリセットする。 割り込み発生時にはtickを停止する。割り込み終了時にはtickを再開する。 これを組み合わせてメイン処理を表現する。 割り込み処理のモデルは、2<=y<=3のときに割り込みを要求してyをリセットする モデルと、メイン処理と割り込み処理の切り替えのモデルを考える。 そして、すべて組み合わせて機能α実現する。 機能αの検査項目は、”デッドロックしない”と”i=1となったら、いずれm=1となる” で、検査式にするとそれぞれ、A[] not deadlockとi==1 -> m==1である。検査結果は、 それぞれ、TrueとFalseであった。つまり、i=1となってもm=0であり続ける事があるの である。 機能Yも同様にしてモデル化できる。 モデル検査の効能は、Falseの反例が得られることにより、思いもよらないタイミングが わかることである。思いもよらない割り込み、思いもよらない初期化もれ、思いもよらな いフラグup、思いもよらないinvariantの崩れなどである。そして、隠れた不備を発見す るための重要な手がかりとなる。 モデル検査の副産物としては、モデル化や検査式の作成から、仕様の細かいところまで 理解が深まることや、仕様の曖昧さがなくなることがある。 組み込みソフトウェア開発へのモデル検査適用に大きな手ごたえが得られた。 組み込み機器はリアクティブである。部分はそうでもないが、組み合わさると一気に複 雑になる。外部環境やハードウェアも含めてモデル化して、実機試験の前に検査できる。 モデルは外部環境とハードウェアとソフトウェアであり、あらゆる可能性をもれなく確 かめられる。 技術者の声としては、検査ツールが不便で時間がかかるといった問題や、設計段階での 検査ができて魅力的といったことがある。 ------------------------------------------------------------------------------ 質疑応答 Q: OS有りだとできるのか等、規模による制限はあるのか。 A: 規模よりも、検査する機能を引っ張り出すのが肝要である。 Q: モデル検査を想定した仕様書はどうやって作るのか。 A: 仕様書から機能を抜き出すので、はじめから機能別にするといった方法がある。 Q: 向いている問題や向いていない問題はあるか。 A: 現在では、プロトコルの検証やハードウェアの検証で実績がある。