CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

Web版 システム検証の事例報告集:概要一覧

事例 1 通信プロトコル設計へのモデル検査適用事例

プロトコルの設計過程の中でモデル検査をして設計を支援した。

事例 2 Webアプリケーションの基本設計書の検証

Webアプリケーションの基本設計で使われる設計仕様からモデルを作るレビュー 手法を提案し、実際の開発済み仕様書の一部に適用する実験を行い、効果を確 認した。

事例 3 Webアプリケーションの画面遷移仕様のモデル検査

Webアプリケーションの基本設計にある画面遷移仕様とプログラム処理の流れ を表わすフローチャート間の整合性をモデル検査で検証する方法を提案し、実 際の事務処理アプリケーションの仕様書に対して適用実験を行った。

事例 4 Webアプリケーションのクラス設計仕様に対するモデル化と検証

Webアプリケーションのクラス設計仕様に対するモデル化と検証手法を提案し、 実際の事務処理アプリケーションの仕様書に対して適用実験を行った。

事例 5 自動検針システム仕様書のモデル検査

自動検針システムの仕様書を題材にモデル検査を行った。仕様書を作成した時 に実施された査読では見つからなかった仕様書中の矛盾、記述不足の不具合を モデル検査で発見することができた。

事例 6 遷移系抽象化アルゴリズムの検証

Lee-Yannakakisによる遷移系の分割縮小化アルゴリズムを形式化し、アルゴリ ズムの正当性と停止性の二つの性質を定理証明支援系PVSを用いて証明した。

事例 7 モデル検査支援装置の基本デザインの検討

モデル検査の支援装置の設計を検討し、特許出願した。 モデル記述言語の習得を必要とせずに、動作仕様からモデル検査プログラムを生 成できる。 検証済みの動作仕様に応じたソフトウェアを自動的に生成することも可能なモデ ル検査支援装置の設計を検討した。

事例 8 アセンブラで記述された組込みシステムのモデル検査による検証事例

原因不明の不正な振る舞いが報告されている組込みソフトウェアに対し,モデ ル検査による検証を行い,モデル化の過程で,脆弱性を一つ発見した.検査対 象は,アセンブラで記述されたソースコードおよび詳細なフローチャートを中 心とする仕様書である.モデル検査は2段階にわけて行った.ソースコードから 半自動的に変換した詳細モデルによる検査と,発見した脆弱性が不正な振る舞 いに繋がるか否かを解析するため抽象モデルによるモデル検査である.詳細モ デルのモデル化の過程でアドレスと値を取り違える不正代入の脆弱性を発見し た.モデル検査器のシミュレーションモードでも脆弱性を確認したが,モデル 検査は,状態爆発により終わらなかった.発見した脆弱性が不正な振る舞いに 繋がるか否かを調べるために,脆弱性に関わる機能の振る舞いをフローチャー トから抽出して作成した抽象モデルによるモデル検査実験を行い,不正代入は 不正な振る舞いには繋がらないであろうという考察をえた.

事例 9 一般公開で用いたLEGO用プログラムの検証

産総研一般公開でCVSは,LEGOを使って作られた車(ロボット)を 操作する簡易プログラム作成を体験する出展を行なった. 展示の際に担当者から,まれに不具合が発生し, 仕様に従った動作をしていないことが報告されたが,原因は不明であった. 不具合の原因を特定するために,モデル検査手法を適用して検証を試みた.

事例 10 確率モデル検査による1次元イジングモデルの検証

自然界や情報科学における確率的な振る舞いを示す系は,確率モデル検査の検証 対象と成りうる. 近年,自然科学と情報科学の境界領域の解析に確率モデル検査が適用され始めて いる. 本研究では,磁性体の簡易なモデルであるイジングモデルに確率モデル検査を適 用し, 従来コンピュータシミュレーションで扱われている物理量に関して 確率モデル検査による解析が可能であることを示した.

事例 11 便益性評価のためのデータ収集実験と評価

形式的技法の便益性評価をする目的で実際のシステム開発のプロセスデータ収集 を行った。また、そのシステム開発に「モデル作成にもとづくレビュー手法」を 適用するプロセスのデータを取得する実験もした。さらにそこで得られたデータ を解析し便益性評価を行った。

事例 12 相互再帰的に定義された文字列を翻訳処理するプログラムの検証

K&Rの教科書第5章の型宣言の文字列を翻訳するプログラムを定理証明支援系PVS 上で形式化し、プログラムが正しく動くことを証明した。

事例 13 たし算かけ算プログラムのコンパイラの正当性証明

整数上の加法と乗法演算のプログラムをスタック操作列へ変換するコンパイラの 正当性をAgda上で検証した.事例自体は対話型証明検証コース初級編の 総合演習とした.

事例 14 非自動はかりの重量データ処理プログラムのモデル検査適用事例

非自動はかりの重量データ処理プログラムの検証にモデル検査を適用した。 勧告OIML R76-1の中の条項 "4.5.7 Zero-tracking device: A zero-tracking shall operate only when the equilibrium is stable." をLTL論理式で記述し、SMV で検証を行った。

事例 15 クルーズコントロールシステムの演繹的検証

オートクルーズコントローラのモデルをAgda上に構築し、基本的な性質の検証を 試みた。

事例 16 Hoare論理の健全性のAgdaによる検証

Hoare論理の健全性証明をAgda上で実行した.

事例 17 Deutsch-Schorr-WaiteマーキングアルゴリズムのAgda-MLAT連携による検証

Deutsch-Schorr-Waiteマーキングアルゴリズムの安全性を,Agda-MLAT連携に よって検証した.

事例 18 ソフトウェア更新システムプロトコルのBAN Logicによる安全性検証

BAN logic は認証プロトコルの分析を行うために与えられた論理の形式体系 である. 本研究では, BAN logic を食品産業向け商品処理装置のために開発 中であるソフトウエア更新システムのプロトコルに適用し, その安全性を検 証した. まず, 与えられたプロトコルについて, その仕様から帰結できる性質を示した. 次に, 通信経路上に悪意のある振る舞いを持つ主体が存在しても「商品処理装 置は最新版の更新プログラムを受信するか, もしくはエラー通知を受信(送信) する」という性質を満たすよう, 最初のプロトコルを変更することによって得 られた2つのプロトコルを与えた.

事例 19 リスト反転アルゴリズムのAgda-MLAT連携による検証

AgdaとMLAT ver.1の連携によりリスト反転アルゴリズムを検証した。

事例 20 TACC業務フロー図の検証

産総研先端情報計算センター(TACC)の人事システムの仕様書の一種である業務フロー図の検証を行った.

事例 21 環境ドライバを用いた組込みシステムのソースコードモデル検査

モデル検査により,既知の不具合の発見可能であるかの調査が目的である.先 の実験で考案した環境ドライバというモデル検査法が適用可能であるかを調べ た.結果として,既知の不具合をモデル検査で発見でき,先の実験で考案した サイクリックエグゼクティブ型組込みソフトウェアに対する効果的なモデル化 法である環境ドライバを用いた方法が本実験でも適用可能であることも示すこ とができた.

事例 22 検証期間の調査のための車載組込みシステムに対するモデル検査実験

モデル検査技術を現場導入するために,検証作業の主要な部分を企業側参加者 が担当し,検査日数を測定した.従来は仕様の検討から検査終了まで2,3ヶ月を 要していたモデル検査による検証が,全体を通じて9日間で終了することが出来 た.また,周期タスク駆動型組込みシステムに対して,抽象などを用いた効果 的なモデル検査プロセスを提案できた.

事例 23 Java の例外処理のSPIN による検証

Java プログラムの例外処理の整合性をモデル検査器SPIN を用いて検証する. Java プログラムでは,発生する例外と例外処理ブロックの内容に不整合が生じ る可能性がある.本実験では,この不整合を発見するためにモデル検査器SPIN と、例外解析器Jex を組み合わせる手法を開発.Jex はJava のプログラム とJava の標準ライブラリを入力とし、そのプログラムが実行時に発生しうる例 外を列挙する.これにより,検証対象のプログラムだけでなく,ライブラリを 起因とする例外処理をモデル化することができる.

事例 24 ソフトウェア更新システムのモデル検査器を使った安全性の検証

近年のコンピューターネットワークの発達に従い、そのセキュリティの確保が改 めて課題となっている。 ネットワーク上でのセキュリティを確保するためには、まずシステムの設計自体 が正しいことが必要であ る。したがって、設計上の誤りをあらかじめ発見する手法が必要とされる。形式 手法は、設計を数学的にモ デル化し、モデルが期待される性質を数学的に証明する。これにより、形式手法 は原理的にはすべての誤り を検出できる。本研究では、株式会社イシダと共同で、形式手法を用いて、同社 の大型商品処理装置内蔵プ ログラムの遠隔更新システムプロトタイプのセキュリティを検証した。まずBAN- logic を用いて、通信さ れる情報がセキュリティを確保するのに十分であることを確かめた。次に、シス テムの詳細仕様書から作 成したモデルを対象にモデル検査を行い、送受信された情報が正しく取り扱われ ているか検証した。

事例 25 Real-Time Maude によるモデル検査と検査式・ モデルの修正

本研究では, 実際のシステムに基づいて作成した架空の生産システムの仕様に モデル検査を適用し, その不具合の発見とその修正を行った. さらに, そのモデル検査のプロセスを考察し, 次の2つに関する提案を行った: 1. 見つけたい反例を選びたすための検査式の作成方法. 2. 対象システムに対する修正の効果と妥当性をモデル検査によって検討する 方法.

事例 26 制御系ECU調停器の演繹的検証

車載ソフトウェアの検証。複数の制御系ECUが発するアクセル・ブレーキ印加 情報を調停し、矛盾のない出力へ統合するユニットを調停器と呼ぶ。ある単純 化された調停器の実装が、調停器としてふさわしい性質を持つことを、対話的 証明支援系を用いて、演繹的な方法で検証した。

事例 27 YAMPIIライブラリ中のポインタ操作のAgda-IVEよる検証

MPI通信ライブラリYAMPIIにおける待ち行列操作の信頼性を、Agda-IVEと pfvalidにより検証した。

事例 28 システムLSI仕様の形式化と検証項目自動生成

システムLSI仕様書を形式化し、それから検証項目を自動生成した

事例 29仕様処理システムの適用実験事例

仕様書の形式化の試験


産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.