HOME>組織の紹介>研究閲覧>検証事例報告集

検証事例報告集

「システム検証の事例報告集」は産業技術総合研究所システム検証研究センターおよびその前身のシステム検証研究ラボなどにおいて平成14年以後に実施した、システム検証の科学技術に関する事例研究を集めたものです。
「システム検証の事例報告集」には、冊子版とWeb版の2種類があります。Web版は、集められた事例を迅速に公開するため、年に数回更新します。冊子版は、年1回年度末に最新の事例報告集が算譜科学研究速報として発行します。

●検証事例一覧

  • 事例1:通信プロトコル設計へのモデル検査適用事例
  • 事例2:Webアプリケーションの基本設計書の検証
  • 事例3:Webアプリケーションの画面遷移仕様のモデル検査
  • 事例4:Webアプリケーションのクラス設計仕様に対するモデル化と検証
  • 事例5:自動検針システム仕様書のモデル検査
  • 事例6:遷移系抽象化アルゴリズムの検証
  • 事例7:モデル検査支援装置の基本デザインの検討
  • 事例8:アセンブラで記述された組込みシステムのモデル検査による検証事例
  • 事例9:一般公開で用いたLEGO用プログラムの検証
  • 事例10:確率モデル検査による1次元イジングモデルの検証
  • 事例11:便益性評価のためのデータ収集実験と評価
  • 事例12:相互再帰的に定義された文字列を翻訳処理するプログラムの検証
  • 事例13:たし算かけ算プログラムのコンパイラの正当性証明
  • 事例14:非自動はかりの重量データ処理プログラムのモデル検査適用事例
  • 事例15:クルーズコントロールシステムの演繹的検証
  • 事例16:Hoare論理の健全性のAgdaによる検証
  • 事例17:Deutsch-Schorr-WaiteマーキングアルゴリズムのAgda-MLAT連携による検証
  • 事例18:ソフトウェア更新システムプロトコルのBAN Logicによる安全性検証
  • 事例19:リスト反転アルゴリズムのAgda-MLAT連携による検証
  • 事例20:TACC業務フロー図の検証
  • 事例21:環境ドライバを用いた組込みシステムのソースコードモデル検査
  • 事例22:検証期間の調査のための車載組込みシステムに対するモデル検査実験
  • 事例23:Java の例外処理のSPIN による検証
  • 事例24:ソフトウェア更新システムのモデル検査器を使った安全性の検証
  • 事例25:Real-Time Maude によるモデル検査と検査式・ モデルの修正
  • 事例26:制御系ECU調停器の演繹的検証
  • 事例27:YAMPIIライブラリ中のポインタ操作のAgda-IVEよる検証
  • 事例28:システムLSI仕様の形式化と検証項目自動生成
  • 事例29:仕様処理システムの適用実験事例

▲ページ先頭へ