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

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

モデル検査

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

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

キーワードで検索する

  • ボンバルディア - 鉄道制御システム
  • Microsoft - Windowsデバイスドライバ
  • Sioux - ホットフード自動販売機
  • Selex Communications - 船舶通信システム
  • 富士重工業 - ECUソフトウェア開発
  • Intertechnique - 航空機の燃料管理システム
  • JAXA - 人工衛星の姿勢制御ソフトウェア
  • Airbus - 航空機システム
  • 日立ソリューションズ - Blu-Rayディスク
  • 日立ソリューションズ - 入退室管理システム
  • Altreonic - 分散RTOS (OpenComRTOS)
  • Samsung Electronics - フラッシュメモリデバイスドライバ
  • Logica Nederland B.V. - オランダ運河のマエスラント防潮可動橋(水門)
  • Philips Healthcare社 - X線CTスキャン
  • POSCON社 - 地下鉄のプラットフォームドア
  • Rockwell Collins社 - パイロット用のディスプレーを管理するシステム

このページの先頭へ戻る

 

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

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