EU
Gemplus - スマートカード
| ドメイン |
|
||||||||||||||||||||||||||||||
| 開発対象 |
|
||||||||||||||||||||||||||||||
| 国 |
|
||||||||||||||||||||||||||||||
| 開発組織 |
|
||||||||||||||||||||||||||||||
| 形式手法（言語、ツール） |
|
||||||||||||||||||||||||||||||
| 適用範囲・規模（形式手法） |
|
||||||||||||||||||||||||||||||
| 適用対象のソフト種別 |
|
||||||||||||||||||||||||||||||
| 適用目的・工程 |
|
||||||||||||||||||||||||||||||
| 実装言語 |
|
||||||||||||||||||||||||||||||
| 実装規模 |
|
||||||||||||||||||||||||||||||
| 効果 |
|
（出典: 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