組み込みソフトウェア開発技術：3.組み込みソフトの検証技術
4
0
0
全文
(2) 3. 組み込みソフトウェアのモデル検査技術入門. ������. ������. ����. ������. �������. �. �. �. �. �. �. ������. �. �������. ����������. 図 -1 プロセス構成. ������. ������. �. �. ����. ������. �. �. � ������. 移ダイアグラムあるいは Statecharts を考えればよい．状 ����������. 態遷移モデルを基本として，適切な通信機構を導入した チャネル通信オートマトンやプロセス代数の考え方でデ ザインを表現する．. ������. ������. �. �. モデル検査の技術. �. � ������. ������. �����������. �����������. モデル検査は，対象を有限の状態空間で表現できるシ ステムに限定し，状態空間の網羅的な探索を行うことで. 図 -2 状態遷移モデル. 不具合を発見する技術である．. ●簡単な例. RESOURCE はプリンタとスキャナを表すプロセスで，. 簡単な並行システムの例を用いて基本的な考え方を紹. 初期状態において獲得 (get) 待ちとなり，その後，解. 6）. 介する ．. 放 (put) だけを受け取る．解放されると初期状態に戻. 図 -1 に示すように，2 つの利用者 P と Q とが，2 つの資. る．P プロセスはプリンタ，ついで，スキャナを獲得し，. 源 Printer と Scanner を使う状況を考える．利用者は. copy 動作を行った後，順に 2 つの資源を解放する．Q プ. スキャナから読み込んだデータをプリンタにコピー出力. ロセスはスキャナを先に獲得する点だけが P と異なる．. する．この作業を行うためには Printer と Scanner の. 図 -2 に状態遷移モデルでの表現を示した．. 2 つの資源を同時に必要とする．資源を獲得した利用者. ||ZENTAI1 は，以上 4 つのプロセスを並行合成した. が作業を完了して解放するまで，もう一方は待たされる．. システム全体を表す．図 -3（a）がシステム全体の状態遷. ところが，資源獲得の順序によっては，互いに相手の. 移記述である．状態 1 から開始したシステムは状態 8 に. 作業完了待ちのデッドロックに陥ることが容易に分か. 至ると出力遷移がないため，これ以降動作を続けること. る．すなわち，P が Printer を獲得し，Q が Scanner を. ができない．状態 8 がデッドロックになる．. 獲得すると，双方とも作業を進めることができない．こ. 図 -3（a）の状態空間を調べると，初期状態 1 からはじ. の問題をモデル検査の方法で見つけることを考える．. まり，デッドロック状態 8 に至る遷移系列は次の 2 つが. 第 1 に，対象となる問題を抽象化して本質だけを抜き. あることが分かる．. 出す．利用者と資源がやりとりする情報として，獲得と 解放だけを考えればよい．以下，この問題を仕様記述言 7）. p.pr.get -> q.sc.get ->. 語 FSP を用いて表現する．. q.sc.get -> p.pr.get ->. RESOURCE=(get->put->RESOURCE) ．. すなわち，この 2 つの遷移系列がシステムをデッドロッ. P=(pr.get->sc.get->copy->pr.put->sc.put->P) ．. クに導くシナリオとなる． モデル検査ツール LTSA を用. Q=(sc.get->pr.get->copy->pr.put->sc.put->Q) ．. いると，上記の FSP 記述をもとに自動的に不具合シナリ 7）. オを求めることができる ． ||ZENTAI1=(p:P||q:Q||(p,q)::pr:RESOURCE ||(p,q)::sc:RESOURCE) ．. 次 に，Q の 記 述 を 変 更 し，プ リ ン タ の 後 に ス キ ャ ナ を 獲 得 す る Q2 と す る．こ の 時 の シ ス テ ム 全 体 は ||ZENTAI2 として定義することができ，また，その挙 IPSJ Magazine Vol.45 No.7 July 2004. 691.
(3) 特集 組み込みソフトウェア開発技術. ��������. ��������. �������� ��������. �. �. �. �. �. �. �. �. �. ��. ��. �. ��. ��. ��������. ��������. ������������. �������� �������� ��������. ��������. �. �. �. �. �. �. �. ��������. �. �������� ��������. �����������. 図 -3 全体構成. ツール（開発機関）. 特徴. 現状. SMV（CMU）. CTL のモデル検査，BDD による高速化. 改版終了？（後継は Cadence SMV）. NuSMV（ITC & CMU）. CTL/LTL, 有界モデル検査 . 公開（SMV の後継）. SPIN（Bell 研）. オートマトンベース Promela. v4.0 公開. LTSA（ICL）. プロセス代数 FSP. 公開（発展中） . CWB（Edingburgh U.）. プロセス代数 CCS, µ- 計算. Concurrency Factory に発展. FDR（Oxford U.）. プロセス代数 CSP. 以前は商用. 表 -1 モデル検査ツール. 動は図 -3（b） になる．. モデル検査の技術に対する素朴な見方の 1 つは，前に 述べた例題のように，システム全体を表す有限の状態空. Q2=(pr.get->sc.get->copy->pr.put->sc.put->Q2) ．. 間を網羅的に探索し，デッドロックなどの不具合を示す 状態の有無を調べることである．特に，これを安全性の. ||ZENTAI2=(p:P||q:Q2||(p,q)::pr:RESOURCE ||(p,q)::sc:RESOURCE) ．. 解析と呼ぶ．どのような状況を不具合とするかは対象問 題依存であるが，先の例では，遷移先を持たない状態を 不具合とした．また，性質を時相論理の式で表現するこ 3）. 図 -3（b）から分かるように，システムはデッドロックの. とも多い ．実際，モデル検査という用語は時相論理式. ない意図通りの振る舞いを示す．. の検証方法からきている． 1970 年代から並行システムの仕様表現と検証を行う枠. ●検証ツール. 組として，時相論理による方法が知られていた．しかし，. 最近は，コンピュータのハードウェア性能が向上した. 検証対象のシステムならびに検証性質の双方を時相論理. こと，状態空間を表現するデータ構造や探索アルゴリズ. の式として表現し，その記述全体が妥当であることを演. ムの工夫などにより，実用的なモデル検査ツールが登場. 繹的に証明するという人手のかかる作業を必要とした．. している．多くは Web 公開されているので容易に入手で. 1980 年代になって，アメリカの E.Clarke グループと. きる．表 -1 に代表的なモデル検査ツールを示す．以下，. フランスの J.Sifakis グループが独立に，時相論理に対す. モデル検査の技術発展を簡単に振り返る．. る自動検査の方法を着想した ．第 1 に，当該システム. 692. 45 巻 7 号 情報処理 2004 年 7 月. 3）.
(4) 3. 組み込みソフトウェアのモデル検査技術入門. の大域的な状態空間を Kripke 構造と考える．第 2 に，そ. これを行うためには，対象システムの特性ならびに検証. の Kripke 構造が命題時相論理式のモデルであるか否か. すべき性質に熟知する必要がある．抽象化したために，. を決定するアルゴリズムを考案し，この決定アルゴリズ. システムが本来持っていた性質が失われてはならない．. ムをモデル検査手続きと呼んだ．特に命題時相論理の. 抽象化の作業は知的な要素が大きく，現状では多くの場. 1 つとして分岐時相論理 CTL（Computation Tree Logic）. 合，ノウハウに依存する．. を導入し，具体的なアルゴリズムを提案した．すなわ. 第 2 に，組み込みシステムの特徴にかかわる課題があ. ち，Kripke 構造 M=(S, R, L) が，有限状態からなる並行. る．協調して全体の機能を果たす複数の状態遷移マシン. システムを表現するとする．ここで，S は状態の有限集. が，同一ハードウェアの上で適切に作動するためには，. 合，R は遷移関係，L はラベルつけ関数と呼ぶ．L は各状. ハードウェアの適切な配分，すなわち，スケジューリン. 態に対して当該状態で成り立つ命題を割り当てる関数で. グを行わなければならない．また，状態遷移マシンに実. ある．次に，当該システムが満たすべき性質を CTL の式. 行の優先順序がある場合，競合する複数のイベント間に. f として表す．この時，モデル検査の問題とは， 「論理式 f. 優先順序がある場合などを考慮する必要がある．外部事. を満たす状態の集合を求めること」, すなわち，. 象に周期性があるなどの時間的な制約を持つこともあ り，時間制約型スケジューリングを行うことも多い．. { s ∈ S |M, s|＝ f }. このようなスケジューリング問題に関しては，独自の 8）. 技術が開発されている ．現状では，モデル検査の技術 を求めることである．. による検証との関係は，個別対応のノウハウとすること. さて，モデルという言葉はソフトウェアの世界で，非. が多い．設計と検証を含めた全体について，系統的な取. 常によく使われる．オブジェクト指向モデリングや分. り扱い方法を整理することが大切である．. 析・設計の方法論，最近の MDA では，プログラムより. 最後に，大量販売・大量消費される組み込みソフト. も抽象的なデザインの記述をモデルと呼ぶ．一方，モデ. ウェアの問題の 1 つとして，リコール時に発生するコス. ル検査検証技法でのモデルとは，論理式（時相論理の式）. トがある．これに対しては，ネットワーク経由の遠隔管. を満たす具体的な集合（Kripke 構造あるいはラベルつき. 理手法による自動置き換えなどの方法も実用化されてい. 遷移システム）のことである．. くと期待できる．しかし，正当な置き換えダウンロード. まとめると，デザインのモデル検査とは，抽象的な記. であるかなどのセキュリティに関連する事項が新たに発. 述である状態遷移モデルから作られる Kripke 構造があ. 生すると考えられる．すなわち，組み込みソフトウェア. り，これが当該システムが持つべき性質を表現した時相. の信頼性確保というと，従来は安全性の点だけを考えて. 論理式の具体的なモデルになっているか否か，すなわち. きた．しかし，今後は，安全性とセキュリティの検証を. 当該論理式を満たすか否か，を解析する検証方法のこと. 同時に考慮する必要があるといえる．. である．. 実用的な技術に向けて モデル検査の技術を組み込みソフトウェアのデザイン 検証に応用する際に問題となる課題を整理する． 第 1 に，モデル検査の技術一般の課題がある．素朴に は，網羅的な探索を行うことが方式の特徴であり，これ が大きな問題となる．探索が終了するためには，状態数 が有限でなければならない．現実的には，検証ツールが 作動しているコンピュータの計算資源の制約がある．す なわち，状態空間がメモリに入りきるか，計算が終了す. 参考文献 1）亘理誠夫 : 高信頼ソフトウェア技術の研究動向− ソフトウェア基礎 技術の確立に向けて−，科学技術動向，科学技術政策研究所，No.24, pp.22-30（Mar. 2003）． 2）システム設計検証技術シンポジウム，独立行政法人産業技術総合研究 所関西センター尼崎事業所（Feb. 2004）． 3）Clarke, E., Grumberg, O. and Peled, D. : Model Checking, The MIT Press（1999）． 4）組込みシンポジウム論文集，情報処理学会ソフトウェア工学研究会 （Oct. 2003）． 5）Lee, E. A. : Embedded Software, Advances in Computers, Vol.56, Academic Press（2002）． 6）中島 震 : モデル検査検証のソフトウェア開発への応用，日本ソフト ウェア科学会 DSW04（Feb. 2004）． 7）Magee, J. and Kramer, J. : Concurrency − State Model & Java Programs, Wiley（1999）． 8）Cottet, F., Delacroix, J., Kaiser, C. and Mammeri, Z. : Scheduling in Real-time Systems, Wiley（2002）． （平成 16 年 6 月 4 日受付）. ることは分かっていても実用的な応答時間で答えが得ら れるのか，などが問題となる． そこで，対象システムを適切に抽象化することが重要 である．設計者あるいは検証者が，あらかじめ対象シス テムを抽象化し適切な規模の状態遷移システムを得る． IPSJ Magazine Vol.45 No.7 July 2004. 693.
(5)
図
関連したドキュメント
なお、関連して、電源電池の待機時間については、開発品に使用した電源 電池（4.4.3 に記載）で
今回工認モデルの妥当性検証として，過去の地震観測記録でベンチマーキングした別の 解析モデル（建屋 3 次元
機関室監視強化の技術開発，および⾼度なセ キュリティー技術を適用した陸上監視システム の開発を⾏う．..
Issuers ; Proposed Rule, No-
