ディペンダブル・システムのための形式手法の実践ポータル

文字サイズ 小 中 大
  • ホーム
  • サイトの主旨
  • 形式手法の概要
  • トピックス
  • 応用事例DB
  • 導入方法
  • 情報源
    • 文献
    • 手法・ツール
    • 会議
    • 公的プロジェクト情報
ホーム > 応用事例DB > 形式手法の分類 > 形式仕様記述

形式仕様記述

形式手法の導入を検討する上で参考となる実システムに対する実践的な応用事例について、費用対効果や導入時の課題・工夫点等を中心にまとめています。

現在は、「フォーマルメソッド導入ガイダンス」第4部付録 12.応用事例情報 と同じ内容ですが、今後事例の数を増やしていく予定です。

キーワードで検索する

  • CSK - TradeOne
  • NSA - バイオメトリクスID認証を利用した入退室管理システム
  • ClearSy - パリ地下鉄プラットフォームドアの制御
  • STS - ニューヨーク地下鉄列車制御システムの最新化
  • ClearSy - 北京地下鉄の自動列車停止システム
  • Lockheed Martin、Praxis - C130Jミッションコンピュータ
  • イギリス国防省 - SHOLIS(ヘリコプタ着陸システム)
  • Mondex International、 Altran Praxis - MULTOS認証システム(Global Key Center)
  • Gemplus - スマートカード
  • National Air Traffic Services (NATS) Praxis - iFACTS、航空管制システム
  • Galois - Trusted Services Engine (TSE)
  • Logica Nederland B.V. - オランダ運河のマエスラント防潮可動橋(水門)
  • Rodin Project - 航空情報表示システム
  • ClearSy社 - コンポーネント仕様のモデル化
  • ClearSy社 - シャルルドゴール空港の無人シャトル制御

このページの先頭へ戻る

 

  • 地域
  • 形式手法の分類
  • 手法・ツール
  • 適用分野

Copyright © Mitsubishi Research Institute, Inc. All Rights Reserved.
このサイトについて 個人情報保護方針 お問い合わせ