SWEST6議事録 分科会２ 「形式的手法を使って楽をする方法」（パネル） 日時：2004/07/23 15:10-16:50 会場：E会場 参加人数：30人前後 -------------------------------------------------------------------------------- コーディネータ：藤倉俊幸（豆蔵） オブジェクト指向の非常に有名な本「Object-Oriented Modeling and Design」の例題に もデッドロックのバグがあるらしい。このバグは形式的手法を用いることで発見できた。 また、組込みシステムの検証において、 ソースコード中心主義だと 　→ソースコードがないとテストできない 　→設計、仕様の時点で間違いを見つけることができない それに対し、設計のテストは設計で、仕様のテストは仕様で行うことができるのが形式 的手法である 。 このことから形式的手法を設計、検証に利用することによって、組込みシステムの開発は もっと楽にならないか？ということをテーマにして分科会を行いました。 形式的手法を利用した設計法や適用例についてパネルによる発表を行って頂きました。 -------------------------------------------------------------------------------- 「大規模事務処理システムにおける形式手法の適用経験」 佐原　伸（日本フィッツ株式会社） ◆なぜ形式手法を用いるのか？ ・論理的根拠 プログラムは数学系である →　C++、JAVAは「検証が困難な数学系である」 従来の手法では検証が困難 →正しくないものを検証するのは事実上不可能 →形式手法では上流から下流に向かって正しさを順に検証 ・経験的根拠 日本語で「正しい」仕様を記述することは困難 →文法や意味の曖昧さ、再利用が困難、ツールチェックが困難 UMLを大規模プロジェクトに適用するのは難しい →仕様記述言語がない、再利用が困難、ツールチェックが困難 ⇒大規模なシステムにおいて、従来技術より形式手法が適用しやすい ◆形式手法を利用した設計適用例 ・対象システム 　株式・公社債・投信などの商品を対象とした、証券会社のバックオフィス・システム・ パッケージの２つのサブシステム ・開発の進め方 　基本的な開発工程は従来のものと同じ >要求定義 >システム仕様作成 VDM++仕様作成 ←形式手法を仕様記述に適用 >プログラミング >管理 ※VDM(Vienna Development Method) ウィーン開発手法と呼ばれる形式手法のひとつ VDM++はVDMをオブジェクト指向に拡張した仕様記述言語 ・生産性 A：マル優サブシステム 見積 38.5人月 実際 14人月 見積/実際 36％ B:オプションサブシステム 見積 147.2人月 実際 60.1人月 見積/実際 41％ ・リリース後のエラー率 形式手法適用部分全体では 0.04 / KDSI ＊他のシステム システム全体 0.67 / KDSI かなりテストされたコード 1.0 / KDSI NASAの難しいコード 0.1 / KDSI ◆まとめ ・形式手法は使えるか？ → Yes しかし魔法ではない ・形式手法は難しいか？ → Yes しかし従来手法やUMLより易しい ソフトウェアを作ること自体が易しいことではない ・形式手法はだれでも使えるか？ → No ソフトウェア科学、構造化の知識が必要 ・形式手法は誰でも管理できるか？ → No ソフトウェア科学の知識が必要 従来手法も誰でも使え、管理できるわけではない 信頼性の高いシステムなどに使えるのではないか。 形式手法は決して簡単ではないが、やるだけの価値はある。 【質疑応答】 Q:ドメイン知識による仕様では問題があるか？ A:ドメイン知識は表記にあいまいさがあり、また仕様を特定の人間だけが理解しているこ 　とになる。 Q:VDMによる開発の進め方は？検証は？ A:検証はすぐにチェック可能 Q:どのようにチェックするのか？ A:シミュレーション 　VDMは言語的な仕様から実行可能な使用まで記述可能である ------------------------------------------------------------------------------- 「形式的言語SDLを使用した組込みシステム開発」 関本　康久（日本テレロジック） ◆SDL (Specification & Description Language) ・ITU-Tによる国際標準規格 ・形式的な言語 ・グラフィカルな表記 ・システムの詳細設計まで記述可能 ・オブジェクト指向に対応 ・実装環境に非依存 ・階層化モジュールとイベント通信 各モジュール間通信、モジュール内部のプロセスの流れはブロック図で表され、 これらは階層構造の記述となっている。 各プロセスの流れはフローチャートで記述。 ・シミュレーション SDLシミュレータ 作成したモデルの動きをトレースして動作検証ができる。 SDLバリデータ 自動的に網羅テストを行いエラー検証を行える。 ◆開発の流れ <設計> 上 要求分析 流 MSC,SDL ↑ システム設計 SDL ↓ コード記述 下 SDL 流 実装 ＊利用ツール　UML2.0 , TAU G2 <検証> 下 流 ユニットテスト ↑ ↓ システムテスト 上 流 リリース ◆SDL利用の効果 　従来手法では工数の進行に伴いエラー率が増加。 　それに対しSDLによる設計ではエラー率の増加量が少ない。 　これは設計工数の早い段階でエラー修正が行われているからである。 　これによりSDLを利用することで開発効率が上がったといえる。 【質疑応答】 Q:フローチャートによる設計は実機に実装可能か？ A:可能である Q:記述が簡単であり、簡単に使えそうであるが、問題点はあるか？ A:コーディングルールに基づいてコーディングを行うため、場合によってはパフォーマン 　スが落ちることがありえる Q:実際に設計したものはあるか？ A:一部設計例をデモンストレーション 　（SDL記述の設計例を表示。ブロック図、フローチャート） Q:SDLで書かれた言語をCに翻訳したとき我々がソースを見て理解できるか？ A:生成されたコードはいきなりは読みづらいが、読むことは可能 　また、チャート図上でデバック可能なツールを開発 Q:バリデータによる検証はどの程度の大きさまで可能か？ A:当然大きくなるほど全探索はつらくなる 　全探索が不可能な場合でも、探索範囲の限定やランダムチェックなど探索時間が発散 　しない方法はある -------------------------------------------------------------------------------- 「モデル駆動系の開発における形式的手法の適用」 倉岡 幹雄（I-Logix Inc.） 組込みシステム開発ツール「Rhapsody」の紹介 「Rhapsody」はUMLに準拠した自動コード生成ツールであり、UMLモデル記述からプログラ ムコードを生成する。 ◆UML2.0 ・状態遷移図の継承が可能 ・コンポジット図、ブロック化モデリングが可能 ・相互作用概要図 ・ライフライン分割 ◆Rhapsody ・モデルからコードを生成 生成可能なプログラムコードはC、C++、JAVA、Ada。 OXFフレームワークによりターゲットのOSプラットフォームにあわせたコード生 成を行う。 --------------------- |生成コード (OML) | --------------------- | OXF | --------------------- | OS(Linux,ITRON) | --------------------- ・リバースエンジニアリング C、C++、JAVA、Adaソースコードからモデルを作成 好きな部分を抜き出してモデルによる確認が可能 ・モデルとコードの同期 モデルから生成したコードを実際に実行させるときに同時にモデルによる動作 確認も可能 ・ビジュアル的なテスト用コンソール あらかじめテストシナリオをシーケンス図で書くことでテストの自動実行が可能 カバレッジテストのテスト環境を構築 モデル図でのテストを行う ◆デモ 電話交換機モデルのテスト モデル上でのテスト動作のデモンストレーション (質問) Q:このテストケースは自動生成したものか？ A:これは手で書いたもの。テストの自動生成も可能である。 生成されるテストはUMLのシーケンス図である。 ビジュアル的に理解がしやすい。 ◆まとめ ・Rhapsodyによる多様なモデル表現能力の提供 ・モデル＝プログラム ・モデルレベルでのテストの実現 手動テスト シナリオベース、テスト自動実行 カバレッジ用テストケースの生成 ・モデルによる開発を行うモチベーションの向上 【質疑応答】 Q:静的なチェックはどの程度行えるか？ A:あまり強くはない。簡単なものなら可能。 Q:開発手順が複雑なのでなにかドキュメントのようなものはないか？ A:ツールを動作させるためのドキュメントはある。 　あくまで開発ツールなので開発工程自体は自由。 -------------------------------------------------------------------------------- 「HW設計で形式的検証をどのように活用しているか」 向山　輝（ＮＥＣ） ◆HW設計フローと形式的検証 ・設計フロー ［RTL］ ↓ ［ゲートレベル］ ↓ ［チップ］ ・等価性検証 RTLとゲートレベルで設計が正しいことを検証 従来より行われている検証方法 ・プロパティ検証 RTL記述での動作検証 モデルチェッキングを行う 実設計では未だ途上技術である ※主にこのプロパティ検証について述べる ◆モデルチェッキング技術 ・モデルチェッキング技術の発展 CTL Model Checking ↓ Symbolic Model Checking ↓ Bounded Model Checking ・Bounded Model Checking サイクル数を限定し、初期からｋサイクルまでを検証 ｋサイクル以内にバグがあれば発見 ｋサイクル以内でなければ発見はできない ◆プロパティ検証の現状 多くのツールベンダが登場 実設計での検証における形式手法の活用状況は２４％程度 ペンティアムの検証に使用された NECではオリジナルのプロパティ検証ツールを開発、又、Cソフトウェアのプロパ ティ検証ツールを試作 ◆プロパティ検証の実用化に向けた課題 ・検証可能規模が小さい フリップフロップの数に対して指数的に増加 ↓ ・現状どのようにしているか プロパティの真偽に影響を与えない範囲で設計を書き換えて規模を縮小 →検証が難しい、検証エンジニア 検証可能規模まで設計を分割 →プロパティ定義が困難に 制約条件をたくさんつける →プロパティ作成にコストがかかる、局所的な検証しか出来ない ・解決するには 計算機、チェックアルゴリズムの進歩 アブストラクション（最小の構造モデル化）の自動化 ・検証すべきプロパティの明確化 何を検証するかわからないといったことが問題になっている。 制約条件は？どれだけプロパティを書けば十分か？ ⇒解決策 -プロパティのライブラリ化 -設計非依存の普遍的プロパティの自動化 -設計方法論の変革 -プロパティ検証はデバッグツールと割り切る -プロパティ記述言語の標準化 ◆形式的検証（プロパティ検証）を使って楽をする方法 プロパティ検証はまだ「プッシュボタンツール」といえるほど成熟していない。 網羅的チェックのメリットはある。 ・現状で使うには しかるべき準備、しかるべき用途に 他のツール（シミュレータなど）に組み込む 仕様レベルでの検証 ・こころがまえ 従来の検証の「プラスアルファ」 バグ検出率を高めるツールと割り切る（100％を保障するものではない） 【質疑応答】 Q:NECで検証ツールを開発しているということだが、これは外部に技術として売り出すも 　のか？それとも自社ノウハウか？ A:NECは現在CベースによるHW設計を行っているが、ツールはこの自社の設計のためのも 　のであり、外部に販売する予定はない Q:ではCベース設計技術に関してはどうか？ A:NEC内の自社技術である -------------------------------------------------------------------------------- 本来７名のパネル発表を行う予定でしたが、時間の関係上下記の３名の発表は中止に なりました。 青木 利晃（北陸先端科学技術大学院大学） 高橋 孝一（産業技術総合研究所） 水口 大知（産業技術総合研究所）