タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
スポンサーリンク
概要
- 論文の詳細を見る
本論文ではタイマを用いる有限状態機械モデルで記述されたシステムに対する検証手続きについて議論する.検証はタイマと有限状態機械からなる系における到達可能な状態の列挙に基づいて行われる.しかしタイマの設定時間が大きい場合, 到達可能な状態数が膨大となるため, 到達可能な状態を列挙するにはメモリや計算時間の点で問題となる.そこでタイマの取り得る値を連立不等式を用いて表し, 複数の状態と状態遷移を一括して扱い到達可能な状態を列挙する手法を提案した.また提案手法による到達可能な状態の列挙に基づく検証手続きを実装し, DHCPに適用した.その結果, DHCPの到達可能な状態を現実的な時間で列挙し, タイマと有限状態機械間のやりとりに不具合がないことを検証することができた.
- 一般社団法人情報処理学会の論文
- 2001-02-20
著者
-
樋口 昌宏
大阪大学大学院基礎工学研究科
-
樋口 昌宏
近畿大学理工学部
-
谷口 健一
大阪大学 基礎工学部
-
谷口 健一
大阪大学大学院情報科学研究科
-
森 亮憲
大阪大学大学院基礎工学研究科
-
徳田 康平
大阪大学大学院基礎工学研究科
-
樋口 昌宏
近畿大学 理工学部 情報学科
-
徳田 康平
大阪大学 大学院基礎工学研究科 情報数理系専攻
-
森 亮憲
大阪大学 大学院基礎工学研究科 情報数理系専攻
関連論文
- データ付時間オートマトンの双模倣等価性の記号的検証法
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 通信プロトコルのエラーリカバリ性自動検証の一方式
- 拡張時間オートマトン群による実時間システムの記述および検証
- 遷移条件が状態訪問回数に依存する有限状態機械対からなる通信系の生存性検証
- 時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,フォーマルアプローチ論文)
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- D-3-6 分散実時間アプリケーションのUML/OCL記述から時間オートマトンネットワークを用いた動作仕様記述への変換手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- 分散環境実時間アプリケーション開発支援のためのTimeliness QoS一貫性検証系および時間制御コード生成系の実装
- 関数型言語ML向け形式的検証支援システムの試作
- 線形制約式を用いた時間QoS一貫性の検証法 (計算機科学基礎理論の新展開)
- 関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
- D-3-8 分散環境における実時間アプリケーション動作仕様記述からのJavaコード自動導出手法の提案(D-3. ソフトウェアサイエンス)
- マルチメディアシステムにおけるTimeliness QoS一貫性検証と時間制御コード導出
- ペトリネットで記述された簡易ブラウザ型の組込みJavaプログラム動作仕様に対する実行方式の提案
- ワークフロー記述向きの時間付きカラーペトリネット
- 時間制約付きカラーペトリネットで記述されたワークフローからのスケジュール導出
- 時間制約を持つGUI制御部の仕様記述の一手法
- 凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
- 入力値のみ保持する変数をもつEFSM群に対する動的性質の検証
- CPU設計導入教育への形式的設計検証手法の適用
- 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
- 1G-6 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
- 複数時間オートマトンによる仕様記述と検証
- 組合わせ幾何を用いた有理数プレスブルガー文真偽判定アルゴリズムにおける投影操作の高速化
- 時間ペトリネットモデルで記述されたサービス仕様からのプロトコル仕様の一合成法
- 拡張有限状態機械とペトリネットを表示編集できるGUIツールの作成と応用例
- 動作実行時刻に制約のある分散システムの全体仕様から各ノードの動作記述の自動導出
- 正則な項書換え系のマルチプロセッサ上での一実現法
- レジスタ付き時間ペトリネットで記述された分散システムの時間制約付き全体仕様からその時間制約を満たす各ノードの動作記述の自動導出(並列・分散)
- 通信プロトコルのフェーズ連結法とそれに基づく検証法
- 有界到達可能性解析を用いた非有界通信プロトコルの解析法
- 拡張有限状態機械でモデル化したOSIセションプロトコルの検証
- 優先サービスを含む通信プロトコルの安全性の検証
- Ambient計算に基づく動的な海上物流の監視システム
- 階層的キーワードベースの名前管理におけるキーワード管理手法
- 非階層型名前空間のファイルシステムへの適用に関する実験的評価
- EFSM適合性試験系列自動生成における系列長短縮化について
- 通信プロトコル適合性試験におけるレジスタ操作に対する試験系列の生成手法(新世代データベース技術 : インターネット・マルチメディア・モーバイルを中心として)
- EFSM に対する適合性試験系列生成手法のミューテーションシステムを用いた実験評価
- EFSM に対する適合性試験系列生成手法のミューテーションシステムを用いた実験評価
- ECFSMモデル通信プロトコル検証のための不変式の半自動生成
- EFSMモデル通信プロトコルの時制に関する性質の一検証法
- 通信プロトコルにおけるレジスタ操作の適合性試験系列生成手法の実験評価
- ECFSMモデルの通信プロトコルに故障耐性機能を付加する一手法
- ECFSMモデルの通信プロトコルの検証のための不変式の自動生成システムの開発
- ECFSMモデルの通信プロトコルへの故障耐性機能の半自動生成
- ECFSMモデル通信プロトコルの検証システムにおける不変式の自動生成
- あるクラスの拡張有限状態機械におけるレジスタ操作の試験系列の生成手法
- 拡張有限状態機械の適合性試験の一手法 : レジスタ代入の正しさの試験
- 拡張有限状態機械でモデル化された通信プロトコルの生存性の検証法
- 拡張有限状態機械モデルの通信プロトコルのlivenessの検証法
- 拡張有限状態機械でモデル化された通信プロトコルのlivenessの検証法
- ネットワークフローを分散制御するプログラム群の一合成法
- 分散計算における制御フローに基づいたイベントアブストラクション手法(マルチメディアネットワークシステム)
- 階層的キーワードに基づく名前管理手法とそれに基づくファイル共有手法
- 階層的キーワードに基づく名前管理手法とそれに基づくファイル共有手法
- 分散環境における透過的なプログラム記述法とD'Agentを用いた実行環境
- 分散環境における透過的なプログラム記述法とD'Agentを用いた実行環境
- 分散データベースにおける通信量を考慮した動的データ配置法
- 逐次化グラフを用いた複合トランザクションの並行制御
- 待ち時間を考慮したΔ因果順序配送アルゴリズムの提案
- 待ち時間を考慮したΔ因果順序配送アルゴリズムの提案
- 配送時間を考慮した因果関係を保存するメッセージ配送
- 部分トランザクションの独立性を考慮した入れ子トランザクションモデル
- 多重化データベースにおけるsite equorumを用いたデータの一貫性制御
- 多重化データベースにおけるsite quorumを用いたデータの一貫性制御
- 多重化データベースにおける仮想分割と再生成を用いた一貫性制御
- 書き込み保留を用いた逐次化グラフスケジューリング
- 分散システムにおける因果関係を保存するメッセージ 配送プロトコル
- 分散型データベースにおける逐次化グラフ検査を用いたスケジューラの実現と評価
- 分散型データベースにおける逐次化グラフを用いたスケジューリングアルゴリズム
- プレスブルガー文真偽判定手続きにおける多元連立1次合同式の求解処理の高速化
- 物流システムに対するAmbient Logicモデル検査システム
- 物流システムに対する Ambient Logic モデル検査システム
- 物流システムに対するAmbient Logicモデル検査システム
- アプリケーション層マルチキャストミドルウェアにおける携帯端末への映像配信機構の実装
- 代数的仕様の作成・検証・実現支援システムにおける公理解析部の生成
- データ転送プロトコルに関する性能要求からのプロトコルパラメータの決定
- タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
- 観測不可能な非決定動作を含む並行DFSM群としてモデル化される通信プロトコルの適合性試験法(マルチメディアコミュニケーションシステム)
- タイマシステムコールを用いるDFSMプロトコルに対する試験系列生成手法(マルチメディアコミュニケーションシステム)
- タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
- 一つのEFSMの複数EFSMによる実現の正しさの一証明法
- EFSM適合性試験系列生成手法の誤実装検出能力の実験的評価
- タイマシステムコールを用いるFSMプロトコルの適合性試験について
- タイマシステムコールを用いるFSMプロトコルの適合性試験について
- 文脈自由プロセスに対するプロトコル合成の一手法
- イベント間の時間制約を論理式で記述できるラベル付き遷移システムとその双模倣等価性検証
- レジスタ付きペトリネットで書かれたソフトウェアプロセス記述の分散実行系
- 拡張有限状態機械モデルで書かれた通信プロトコルの適合性試験系列の自動生成の一手法
- プログラム検証支援のためのプレスブルガー文真偽判定ルーチンの高速化
- マルチスレッド機構を用いたLOTOS仕様実行方式とその評価
- 拡張有限状態機械モデルにおける通信プロトコルのテスト系列の自動生成の一手法
- 代数的手法を用いた回路設計支援システムにおける状態図簡約機能とその評価
- 通信系の動作記述から各局のプロトコルマシンを生成するための一方法
- 時間付きAmbient Calculus