Comments
Description
Transcript
講演資料 - IPA 独立行政法人 情報処理推進機構
形式手法を用いた実践的開発への取り組み ～ 北海道での形式手法の取り組み ～ 第14回 組込みシステム開発技術展 情報処理推進機構 ブースセミナー 2011年5月13日（金） 北海道電子機器株式会社 （地独）北海道立総合研究機構 穴田 秀樹 堀 武司 北海道での取り組み ・札幌を拠点とする民間企業を中心にして → 実践的な形式手法導入への取り組み Ｂメソッドによる開発 ・産業界での応用 → 中小企業の「ものづくり視点」での導入 ・形式手法への取り組み → 高信頼なソフトウエア開発の要求への対応 戦略的基盤技術高度化支援事業 ・平成２２年度 経済産業省 戦略的基盤技術高度化支援事業に採択 ・北海道経済産業局 平成２２年度 情報政策の重点取り組みについて ・ＩＰＡのバックアップ 支援事業にて、技術的アドバイス 実施例） 形式手法を用いた開発プロセスレビューなど 研究機関 北海道電子機器（株） （株）ミクロスソフトウエア （株）リック （株）ヴィッツ （地独）北海道立総合研究機構 （独）産業総合研究所 北海道大学 ７機関の連携 企業紹介 － 北海道電子機器株式会社 会社概要 社名 北海道電子機器 株式会社 所在地 北海道札幌市東区北10条東10丁目1-1 設立 昭和５２年９月 従業員数 ２４名 業務内容 ハードウエア ・ ソフトウエア ・ 機構 ハードウエア開発／組込みソフト開発 設計・製作・販売 当社は創業以来、計測制御関連の組込みシステムを、 ソフトウエア・ハードウエア技術により、提供してきました。 基本設計・開発・製造・現地試験までの一貫した ものづくり体制で、お客様のニーズに対応します。 機構設計 得意分野 ： センサー微小信号処理、低消費電力回路 対応デバイス ： SH、H8、R8C、SHARC、FPGA お問い合わせ 当社HPより http://www.hdks.co.jp TEL 011-748-3666 FAX 011-748-3660 多目的データロガー Ｈｉ・Ｐｅｒ 企業紹介 － 株式会社 ミクロスソフトウエア HP：http://www.micros.co.jp/ TEL：044-813-7211 ミクロスソフトウェアの会社概要 会社名 株式会社ミクロスソフトウェア 創業 1983年2月23日 従業員数 103名 （2011年4月1日現在） 所在地 FAX：044-850-1655 ミクロスソフトウェアの製品／サービス ハイビジョン映像送出装置 GUIによる送出画像のデザイン・レイアウトの編集機能の提供や他システムから取得したデ ータを送出画像に取り込む等、フレキシブルなデータ連携を取ることが可能な「ハイビジョン 映像送出装置」のソフトウェアとハードウェアを共に提供している。 NHK放送にて、為替、 株価などの経済情報を いち早く、正確に伝える 為の放送システムとして 現在利用されている。 本社 神奈川県川崎市 北海道支社 北海道札幌市 北見事業所 デバイス仮想化技術 北海道北見市 <本社> 資本金 1億円 取得認証 ISO9001 / ISO14001 / ISO27001 /プライバシーマーク <札幌> 組込製品に搭載されるOS（NetBSD）上のデバイスを 仮想化し、製品システムのシミュレータ開発を行って いる。 ・デバイスドライバの擬似化と デバイスシミュレータ開発 ・カーネル割込制御、デバイス認識コントロール ・DMA転送シミュレーション ・メモリデバイスの仮想化 ・カーネル管理情報の動的変更制御 ・共有メモリ管理、メモリマップ変更 地図データオーサリング開発技術 JQA-QM4262 主な事業 JQA-EM3675 JQA-IM0584 ・カーナビゲーションシステム開発 ・携帯電話ソフトウェア開発 ・TV放送データ配信システム開発 ・複合機のドライバー/ミドルウェア開発 プライバシ ー カーナビゲーションシステム の開発で必要とされる、道路 データ、経路探索データ、音 声認識データなど全てのデー タのオーサリングツール開発 が可能。 国内の大手地図メーカーが 提供する地図に加え、海外の 主要地図メーカーの地図デ ータの作成が可能。 企業紹介 － 株式会社リック 会社概要 商 号 所在地 設 立 従業員数 業務内容 株式会社リック 北海道札幌市北区北6条西1丁目3番地 38山京ビル9F 平成7年1月 28名 業務系ソフト受託開発・組込系開発・技術支援・ハードウェア販売 パッケージソフト開発及び販売・研究開発など ハンディターミナル開発 ハンディターミナルによる 各種(ガス・水道・電気)の 検針業務アプリ開発や、 実績情報のリアルタイム 収集システム開発などを 手がけております。 検針が困難な箇所の メーターと無線で通信して 行う無線検針の通信ライブラリ などの開発も手がけています。 複合機 meap開発 あらゆる業種の様々な顧客 に対応する為の複合機専用 の開発環境にてﾌﾟﾘﾝﾃｨﾝｸﾞ ﾃﾞﾊﾞｲｽとして、FAXやPDF 加工など様々なAPIを駆使 して制御する為の開発を 行っています。 モバイル向けUIツール開発 モバイル向けに、画面遷移等を行なうライ ブラリ、UIデザインを構築するツール、各 種プラグインの開発を行なっております。 【お問い合わせ】 リックWebサイト http://www.lic.ne.jp/ （リックサイト内の「お問い合わせフォーム」もご利用下さい。） TEL 011-708-5501 FAX 011-708-5502 形式手法の活用 ・形式手法の導入は？ 導入の敷居は低い！ → 中小企業でも、取り組みが可能！ ・記述してみると？ 形式的仕様記述である。 プログラムを記述しているのではない。 → プログラム的な考えでは、うまくいかない・・・。 新しい手法には、新しい考えをしないと。 この後の、技術的内容にて、ご紹介します！ 目次 Bメソッドの紹介 手法概要・産業界での適用実績 Bメソッドによる開発の流れ 仕様検証の仕組み … 何が検証できるのか？ 導入にあたってのポイント Bメソッドの利点、課題点 他手法 (Z, VDMなど) との比較 まとめ Bメソッド 概要 概要 Z記法 や VDM と同じ、モデル規範型の形式記述手法の一つ Z記法の設計者の一人でもあるJean Raymond Abrialを中心として、 1980年代後半に開発された。 (ZやVDMと同様に) 集合論と述語論理を用いて仕様記述を行う 設計・開発手法全体を含む「メソッド」である (単なる仕様記述言語ではない) 形式的仕様記述～段階的詳細化～実装～コード生成 各工程における形式的検証 産業界での利用 欧州を中心に、産業界での実績が多数存在する。 パリ地下鉄14号線 自動運転システム など 実用に耐える水準の支援ツールが提供されている。 支援ツール Atelier-B (仏 Clearsy社) Bメソッド本来の検証方法(定 理証明）を行うツール 機能 文法チェック・型チェック 証明責務(PO)の生成 自動定理証明系による POの証明支援 コード自動生成(Cほか) V4.0からは、製品版が無償 公開されている。 支援ツール ProB Animator and Model Checker(独 duesseldorf大 他) B仕様記述に対して、仕様ア ニメーションとモデル検査 を行うためのツール 機能 シミュレーション実行（対話/ ランダム) モデル検査 状態の網羅的探索 デッドロック等の検出 時相論理式(LTL, CTL) 状態遷移グラフの可視化 無償で利用可能 Bメソッドによる開発の流れ 「正しい仕様・設計」から「正しいプログラム」を導出する。 “Correctness by Construction”の考え方 要求 仕様検討 抽象機械 Bツールによる検証支援 構文・型検査 証明責務生成/証明 構文・型検査 証明責務生成/証明 構文・型検査 証明責務生成/証明 設計検討 詳細化 設計検討 実装 自動コード生成 プログラム B抽象機械 (Abstract Machine) MACHINE 機械名称 (パラメータ, ...) VARIABLES 変数名, ... INVARIANT 変数の型宣言 & 抽象機械の不変条件 INITIALISATION 変数の初期化処理 OPERATIONS 出力変数 操作1 (パラメータ, ...) = PRE 事前条件 THEN 操作の処理内容 END END 出力変数 操作2 (パラメータ, ...) ... END • 抽象機械 – 状態＋操作をカプセ ル化したもの – 状態：状態変数 – 操作：状態変数の書 き換え規則 • プログラム言語との違い – 不変条件：抽象機械 の状態が常に満たし ているべき条件 – (操作の)事前条件：操 作の実行時に満たさ れるべき条件 – 集合論と述語論理に 基づく文法 簡単なB抽象機械の記述例 Booking (座席予約) MACHINE Booking (max_seat) CONSTRAINT max_seat ∈ NAT VARIABLES seat // 残り座席数 INVARIANT seat ∈ 0 .. max_seat // 整数の部分集合であり // 0～max_seatの値をとる INITIALISATION seat := max_seat OPERATIONS book = PRE 0 < seat THEN // 座席が1以上なら予約可 seat := seat – 1 END; cancel = PRE seat < max_seat THEN // 最大数以上は返却不可 seat := seat + 1 END END • 概要 – 座席の予約、キャンセル • 抽象機械の記述 – 状態 • 現在の残り座席数 – 操作 • 座席を予約する • 予約キャンセル • 通常のプログラム言語の記 述に近い Bメソッドによる検証のしくみ 何が出来るのか？ ・抽象機械の「整合性」の検証 仕様記述の一部として、「不変条件」と呼ばれる条件式を記述する。 → 不変条件が常に成立していることを保証出来る ・段階的詳細化の過程が正しいことの検証 抽象機械（モジュールの外部仕様）を記述 詳細化機械（具体的な実現方法・実装方法）を記述 → 詳細化の過程が正しいこと（仕様に矛盾しない実装であること） を、検証出来る 具体的な仕様検証の方法 定理証明による方法 仕様記述から「証明責務」(Proof Obligation)とよばれる証明問題を生成 POを全て証明できた → 仕様の整合性が保証 証明作業は、主に自動定理証明プログラムで行う 検証作業には、専門知識と工数が必要 モデル検査による方法 状態空間を網羅的に探索し、不変条件が偽になる状態がないか調べる。 検証作業はツールによる自動実行。 状態空間が広い、または無限の場合、検証作業は困難になる。 Bメソッドでは、両方のツールが提供されている。 手法の特性に合わせて、使い分けが可能！ 不変条件の設定 車速・ロックボタンとドアロック状態の関係を、不変条件として整理してみた。 車速15km以上ならば、ドライバ席はロック状態でなければならない。 車速15km以上、または全ロックボタンONならば、助手席はロック状態でなければならない。 車速15km以上、または全ロックボタンON、または左チャイルドロックONならば、左後席は ロック状態でなければならない。 車速15km以上、または全ロックボタンON、または右チャイルドロックONならば、右後席は ロック状態でなければならない。 INVARIANT ..... /* システムの不変条件 */ (speed >= 15 ⇒ l_driver=lock) & ((speed >= 15 or b_al=b_on) ⇒ l_codriver=lock) & ((speed >= 15 or b_al=b_on or b_cl=b_on) ⇒ l_rear_L=lock) & ((speed >=15 or b_al=b_on or b_cr=b_on) ⇒ l_rear_R=lock) 上記の内容が常に真であることが、形式検証によって保証できる。 ドアロック管理システム 操作の記述 操作として記述したモデルの振る舞いが、不変条件と矛盾していない事を、数学 的に示すことが出来る。 OPERATIONS // 助手席ドアのロック/解除 unlock_codriver = PRE l_codriver=lock & speed <15 & b_alllock=b_off THEN l_codriver := unlock 速度と全ロックボタンの END; 状態を、事前条件に記述 lock_codriver = PRE l_codriver=unlock THEN l_codriver := lock END ツールによる反例の発見 • • 発見された反例 – speed=0 (停車状態) – 助手席ロック解除 (speed<15 なので可能な操作) – speed=15 (車が動き出した) – × 車速15km以上、または全ロックボタンONならば、助手席はロック状態でなければな らない 対処 – 車速が15km/hを超えると、自動的にドアをロックする機能を追加。 – ロック解除禁止ボタンについても同様の不具合があったので、仕様を修正 set_speed (ss) = PRE ss : NAT & (ss=0 or ss=15 ) THEN IF ss < 15 THEN speed := ss ELSE speed := ss || l_driver := lock || l_codriver := lock END END; 全ての状態で不変条件が満たされている 事を確認 初期仕様の不整合を見つける Bによる形式的仕様記述 不変条件による記述 What 寄り 漠然とした 要求仕様 矛盾 操作の記述 How 寄り 異なる観点から記述する事で、仕様の不整合に 気づくことが出来る。 Bメソッド導入のポイント 形式手法未経験の中小企業エンジニアが、一年間 Bメソッドに取り組ん できた H22年度： 形式手法の調査、開発の準備 H23年度～：実開発(模擬プロジェクト)への適用と、効果の測定 その経験に基づき ・技術導入にあたってのポイントとなる事項 ・陥りやすい問題点 について、いくつか紹介します。 Bの記述は、制約が厳しい 抽象機械 Foo.mch 詳細化 Foo.ref 実装 Foo.imp ・同時実行文のみ記述可能 ・逐次実行文の記述は禁止 どちらでも使える モジュールの インターフェース (引数・戻り値）は 最初に決めたものから 変更出来ない ・同時実行文は禁止 ・逐次実行文のみ記述可能 ・抽象的なデータ型は使用出来ない 同時実行・逐次実行文の記述、利用出来るデータ構造、インターフェースの変更などにつ いて、かなり厳しい制約がある。 抽象機械～詳細化～実装のフェーズによって、ルールが180度変化する 初学者が非常に戸惑いやすい点 厳しい制約は、必ずしも の欠点ではなく、利点でもある 記述制約により、Bメソッドの方向性に沿った開発が可能 抽象機械 Foo.mch 逐次実行文が禁止されているので、 プログラム的な処理手順を書こうと 思っても書けない。 What を書くことを「強制」される 詳細化 Foo.ref 実装 Foo.imp 抽象機械で定義された仕様を 実現するための、具体的な処理手順 Howを記述する。 ・一般のソフト技術者は、仕様(What)を書くべき局面でも、プログラム的な処理手順(How) を記述してしまいがちである。 → 各フェーズの記述の制約によって、Bメソッドらしい記述が「強制」される。 ・その他の制約も、Correctness by Construction に基づく設計・検証を実現するために必 要なもの 逐次処理でなければ表現出来ない場合 MACHINE Demo OPERATIONS // 抽象機械では空の処理 // として記述 IMPLEMENTATION Demo_i REFINES Demo : OPERATIONS // 詳細化段階で、逐次処理として記述 run = skip run = VAR sw1, sw2, sw3, sw4, disp IN disp get_lcd_disp; IF sw1=TRUE & pre_sw1=FALSE : END END ・しかし、実際の開発の局面では、逐次処理でなければ表現出来ない仕様も多い。 ・一応、記述は可能だが、Bメソッドを使う利点の多く(詳細化過程の正しさの検証など)は失われ てしまう事に注意。 Bメソッドを適用しやすい・しにくい対象 実際の開発においては、B言語の記述能力や、コードジェネレータの制 約が、技術的な障害になる事も事実 適用しやすい対象 ブール値、整数、列挙型などだけで表現できるもの 静的なデータ構造のみを扱うもの （小規模な組込み制御システムの多くは、これに該当する） → 現行の設計技法、ツールチェインでも、十分実用的な開発が 可能。コード自動生成も可能。 (現状では)適用しにくい対象 動的なデータ構造、可変長データ、文字列や、それらの受け渡しを 伴うもの（例えば、プロトコルスタックなど） → データ構造をライブラリ(基本機械)の中にうまく隠蔽するなど、 設計の工夫が必要 適切な不変条件の設定が重要 Bメソッドの検証 不変条件が常に成立する事を証明する (与えられた前提の元で) 100% 保証出来る。非常に強力。 → しかし、適切な不変条件の設定を行わなければ、実際に意味のある検 証は実現出来ない 課題: 仕様から適切な不変条件を導出するのが難しい 一般のソフト技術者は、動作中心の物の見方に慣れ過ぎており、対象を不 変条件として静的に捉えるための訓練が必要。 元の要求仕様自体が、動作中心に構成されていたり、最初からHow のレ ベルで記述されている場合も多い。 「書くべき不変条件が、見つかりません！」 仕様からの不変条件抽出の事例 ・各システム状態での振る舞い 初期状態ならば、 (LED1=ON & LED2=ON)である 計測状態ならば、 (LED1=点滅 & LED2=OFF)である 通知状態ならば、 (LED1=OFF & LED2=点滅) 安全に関する条件 薬品の加熱時間 は (180+マージン)秒より も短い 出典:金周慧、松原豊、高田広章、”状態遷移図に着目した安全要求分析手法”、第8回クリティカルソフト ウェアワークショップ、2011 他手法(VDM, Z記法)と Bメソッドの比較 Bメソッドは、Z記法よりも現場で使いやすく、VDMよりも検証能力が高い。 VDM Z記法 Bメソッド 記法 プログラム的 数学的 ややプログラム的 段階的詳細化 △ △(可能) ○ 形式検証 仕様アニメーション 中心 ツールによる 定理証明 モデル検査 アニメーション コード生成 Javaなど ツールによる C、Adaなど 記述の自由度 高い 高い 制約が厳しい 支援ツール 充実 弱い 充実 VDMtools ZETA, CZT, Atelier-B, ProB overture HOL-Z など まとめ ・Bメソッドの特徴と利点 単なる仕様記述だけでなく、設計開発方法論がある程度確立して いる。 Correctness by Construction の考え方に基づく、厳密な仕様記 述・検証を伴った開発が可能。 実用的な開発が可能な環境（手法・ツール）が整備されている。 ・技術導入のポイントと課題 記述の制約が厳しいのが、欠点であり利点でもある（設計・検証を 正しい方向に導くための制約） プログラム的なHowではなく、What の観点で記述する訓練が必要 検証能力を活かすには、不変条件の適切な記述が重要 謝辞 本発表は、H22～24年度 経済産業省 戦略的基盤技術高度化支援事業（北海道経済産 業局）の採択テーマとして実施中の「形式的仕様記述を用いた高信頼ソフトウエア開発プ ロセスの研究とツール開発」の成果を利用しています。 本資料および開発等に関し、プロジェクトのメンバならびにアドバイザ各位に感謝すると 共にここで紹介させていただきます。 研究実施機関名 北海道電子機器㈱、㈱ミクロスソフトウエア、㈱リック、㈱ヴィッツ 北海道大学、(地独)北海道立総合研究機構、(独)産業総合研究所 アドバイザー機関名 名古屋大学、苫小牧工業高等専門学校、㈱日本除雪機製作所 北海道日本電気ソフトウエア㈱、トヨタ自動車㈱、アイシン精機㈱、 ルネサスエレクトロニクス㈱