EU

Gemplus - スマートカード

ドメイン
    電子部品・デバイス
開発対象
    スマートカードのOS
    フランス
開発組織
    Gemplus
形式手法(言語、ツール)
    B (Atelier B)
適用範囲・規模(形式手法)
    一部のコンポーネントにのみ適用
適用対象のソフト種別
    制御系
適用目的・工程
    設計、コード生成
実装言語
実装規模
効果
    最終的な開発工数を削減することができた。
      形式手法を利用した開発 従来型の開発
    開発 12週間 12週間
    検証 6週間 NA
    テスト 1週間 3週間
    統合 1週間 2週間
    合計 20週間 17週間
    レビューによるバグの発見数 13 24
    証明によるバグの発見数 29 NA
    テストによるバグの発見数 32 71
    合計 74 95

(出典: Industrial Use of Formal Methods at Gemplus, Gemplus Research Lab)


詳細情報

検証内容

  • あるJavaアプレットが他のJavaアプレットのデータにアクセスできないこと
  • JavaアプレットがOSのコードにアクセスできないこと
  • 正しいモデルを作成し、Atelier Bで自動証明を行った
  • 残った証明に関しては、対話式証明を行った。対話式証明により、モデルやループにおける不変条件の不備やそれらをどう構築すれば良いかを理解することができた

検証規模

期間

判断

形式手法を利用した動機

    スマートカードの高いレベルでの認証が必要だった。また、検証コストを削減する必要があった。

手法・ツール選択理由

障害と工夫

  • 最初のBモデル仕様のレビューをしっかり行った
  • Atelier Bの自動証明に適合するようにモデルをチューニングした

組織

体制

教育

その他

情報源

    Jean-Louis LANET, The use of B for Smart Card

このページの先頭へ戻る