時制論理に基づくプロトコルの LOTOS 仕様の合成
スポンサーリンク
概要
- 論文の詳細を見る
プロトコル等,通信システムの仕様を曖昧なく記述するために,種々の形式記述技法が開発されている.これらの形式記述技法は数学的に厳密な取り扱いができる反面,記述が局所的であるために,仕様の大局的な振る舞いを陽に表現することができないという欠点がある.そのため,形式記述技法で記述された仕様が安全性,生存性等の時間的性質を満足しているかどうかを直観的に判断することは一般に困難である.一方,時系列上の性質を表現するために構成された論理体系が時制論理である.時制論理を用いると時間的性質を陽に表現することができ,大局的な振る舞いを理解しやすい.本論文では,形式記述技法の一つであるLOTOSを取り上げ,その意味を表すラベル付き遷移システム上で拡張分岐時制論理を定義する.そして,この論理で記述された時間的性質から,それを満足するLOTOS記述を導出する方法を提案する.さらに,より詳細な時間的性質を加えることで仕様を詳細化する方法も併せて提案する.これにより,時制論理を基礎とする段階的な仕様化が達成できる.また,時間的性質としてプロトコルの生存性を与えると,あるクラスのプロトコルのLOTOS仕様が得られ,この方法がプロトコルの仕様を与える上で有効であることを示す.
- 社団法人情報処理学会の論文
- 1993-06-15
著者
-
加藤 靖
仙台電波工業高等専門学校
-
高橋 薫
仙台高等専門学校
-
加藤 靖
仙台電波工業高等専門学校情報工学科
-
安藤 敏彦
仙台電波高専
-
安藤 敏彦
仙台電波工業高等専門学校
-
高橋 薫
東北大学電気通信研究所
-
野口 正一
東北大学応用情報学研究センター
-
安藤 敏彦
仙台電波工高専
-
野口 正一
日本大学工学部情報工学科
関連論文
- 睾丸腫瘍及び膀胱癌の腫瘍組織内リンパ球 Subpopulation
- 変数を用いたWebアプリケーションのモデル化と形式的手法による検査(ワークショップ(査読付き),「次世代経営情報技術」,その他)
- 形式的手法によるWebアプリケーションのモデル化と検証
- 先天性水腎症における尿輸送能の定量的評価法の研究
- 両側異時発生セミノーマの3例 : 第188回東北地方会
- オントロジを利用した健康支援システムの提案とその評価(Webインテリジェンス,情報洪水時代のネットワークサービス)
- 1B-3 画面遷移を用いたWebアプリケーションのモデル化とSPINによる検証(プログラム検証と品質管理,一般セッション,ソフトウェア科学・工学)
- Webアプリケーションの変数を用いたモデル化と形式的手法による検査
- オントロジを利用した健康支援システムの設計と実装
- F_010 オントロジに基づいた健康アドバイス導出システム(F分野:人工知能・ゲーム)
- F_009 健康アドバイス導出のための領域オントロジと推論ルール(F分野:人工知能・ゲーム)
- F_008 Bluetooth通信を用いた生体情報監視システムの構築(F分野:人工知能・ゲーム)
- 健康に関する領域オントロジと健康アドバイス導出ルールの構築(経営や情報技術双方の知識や立場を越えた相互理解を醸成するモデリング及びモデリングフレームワークを研究する : 特に今回はセマンティックWEBの活用にフォーカスする)
- 状態遅延と入力遅延を導入したオートマトンによるディジタル論理とPLCの仕様化
- オントロジーに基づいた暗号学習用のe-Learningシステム(e-Learning教育システムの成果と目指すべきもの/一般)
- オートマトンモデルに基づいたディジタルロジックの仕様化と検証
- 状態マシンモデルに基づいたセキュリテイプロトコルの仕様化
- エージェントによるファイル交換システム
- エージェントによるアプリケーション共有
- 種々の手法によるディジタルロジックの仕様記述とそれらの比較
- 複数グループ間におけるスケジュール調整支援システムの開発
- オブジェクト指向を導入した状態マシン記述
- 比較的まれな副腎腫瘍の5例(偽嚢腫,リンパ管腫性嚢腫,骨髄脂肪腫,脂肪腫,神経鞘腫)(第197回東北地方会)
- 上部尿路の低流量Pressure-Flow Study : 第74回日本泌尿器科学会総会
- 経口剤による尿酸結石溶解症例について : 第194回東北地方会
- モノクローナル抗体,レクチンを用いた膀胱腫瘍の研究
- A State Machine with Time Constraint
- エージェントフレームワークDASHを用いたスケジュール管理システムノ設計ト実装
- 契約ネットプロトコルの形式的仕様化と解析
- 状態マシンモデルに基づいた並行システムの複合的仕様化手法
- 命題論理に基づいた並行システムの制約付き仕様記述
- 場と有限状態機械の概念に基づいたモバイル並行システムの仕様化手法とその適用(マルチメディアコミュニケーションシステム)
- 有限状態モデルに基づくモバイルシステムの仕様化
- 移動性を考慮した有限状態モデルに基づく並行システムの仕様化
- 動的再構成システムの仕様化と検証
- PBL手法に基づいた産学連携の実践的ソフトウェア開発教育(情報システム教育コンテスト(3))
- (41) マルチタスクOS教育用マイクロコンピュータシステムの開発(第2セッション 教材の開発-II)
- (40) スパイラル方式に基づくマイクロコンピュータ応用技術教育の実践方式(第2セッション 教材の開発-II)
- (39) 基礎原理の理解を目指した論理回路実習用ボードの開発(第1セッション 教材の開発-I)
- (38) 高専における体系的ディジタル技術教育の実践(第1セッション 教材の開発-I)
- 高専における実践的マイクロコンピュ-タ教育の一方法
- Composition Method of Service and protocol Specifications
- 並行計算πFを用いたモバイルシステム管理
- 動的再構成システム仕様の挙動検証
- 地理的制約を考慮した並行計算
- 位相的観点に基づく段階的仕様記述
- 位相的観点からの仕様記述
- 時制論理に基づくプロトコルの LOTOS 仕様の合成
- LOTOSに基づいたプロトコルの論理検証支援システムの実現
- LOTOS仕様の分割支援システム
- μITRONに準拠した16ビットボ-ドコンピュ-タシステムの開発
- セル構造オ-トマンの様相集合の特性化
- 一次元一様構造オ-トマトンの安定様相について-2-安定様相の個数及び増加率
- 一次元一様構造オ-トマトンの安定様相について-1-安定様相の生成能力に関する関数の類別と等価変換
- 形式的手法によるWebアプリケーションのモデル化と検証
- オブジェクト指向を導入した状態マシン記述
- シェイクスピア劇を親しむための方法と実践
- Webアプリケーションの変数を用いたモデル化と形式的手法による検査
- 相互接続試験への拡張性を考慮した適合性システムの開発
- 適合性試験システムの開発 : IUTシミュレータの開発
- 相互接続試験システムAICTSの開発 : 試験スイートの検討
- 相互接続試験システムAICTSの開発 : プロトタイプの開発
- 並行計算πFを用いたモバイルシステム管理
- 有限状態モデルに基づくモバイルシステムの仕様化
- 傍膀胱肉腫の1例 : 第185回東北地方会
- シアターゲームにおける非言語コミュニケーション
- シアターゲームにおける非言語コミュニケーション(コミュニケーション支援及び一般)
- シアターゲームにおける非言語コミュニケーション(コミュニケーション支援及び一般)
- LOTOSによるCCRサービス定義の形式記述 : データ型部 : INTAP研究開発委貝会プロトコル形式記述WG
- LOTOSによるCCRサービス定義の形式記述 : プロセス部 : INTAP研究開発委員会プロトコル形式記述WG
- LOTOSによるCCRサービス定義の形式記述 : 全体報告 : INTAP研究開発委員会プロトコル形式記述WG
- 2Z-4 プライバシーを考慮した個人・組織情報検索システム(人工知能一般(3),学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- F-036 OWLによる個人・組織情報のモデル化とプライバシーの取扱い(人工知能・ゲーム,一般論文)
- 並列性を考慮した通信システムの相互接続度験系列生成法
- 並列性を考慮した通信システムの相互接続試験系列生成法
- プロセスの独立性を考慮した通信システムの相互接続試験系列生成法
- 並列試験系列記述法PTSNを用いた試験の効率に関する一考察
- J-037 非言語コミュニケーションの分散協調モデル(J分野:ヒューマンコミュニケーション&インタラクション)
- 2Z-6 NuSMVを用いたオントロジ検証(人工知能一般(3),学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 2P-2 形式的手法と検査ツールによるモデル検査事例と考察(ソフトウェアの検査・検証,学生セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- B-015 モデル検査を用いたオントロジの検証(ソフトウェア,一般論文)
- J-002 仮想物体を用いたシアターゲームおける身体協調(ヒューマンコミュニケーション&インタラクション,一般論文)
- シアター・ゲームにおけるコミュニケーション(ヒューマンコミュニケーショングループ(HCG)シンポジウム)
- 2次元セル構造オ-トマトン動作解析ソフトの開発
- 高度化再編による仙台高専の誕生
- H-036 身体モデルを用いた3Dモーションキャプチャ(H分野:画像認識・メディア理解)
- パフォーミングアートにおける演技者のコミュニケーション
- セルモデルコミュニケーションにおけるパターン形成
- セルオ-トマトンにおける動的振舞いの可視化に関する一考察
- D-3-5 NuSMVを用いたRBACモデルの検証(D-3.ソフトウェアサイエンス,一般セッション)
- 自学型習熟度別プログラミング教育の実践
- 国際交流を中心とした海外研修旅行が学生にもたらす効果
- 地域に開かれた高専を目指した取組み
- B-016 ロールオントロジーに基づいた個人・組織情報への動的なアクセス制御(開発支援・プロジェクト管理,B分野:ソフトウェア)
- B-005 モデル検査ツールNuSMVを用いたオントロジー検証(テスト・検証,B分野:ソフトウェア)
- B-023 RBACモデルの形式検証(電子文書・ソフトウェア科学,B分野:ソフトウェア)
- ユーザコンテキストに基づいた個人・組織情報へのアクセス制御(経路・アクセス制御,応用,インターネットやイントラネットの信頼性,品質,計測,監視,セキュリティ,トラヒック理論及び一般)
- A-7-11 ユーザコンテキストに基づいた個人・組織情報へのアクセス制御(A-7.情報セキュリティ)
- D-3-2 RBACモデルの検証支援ツール(D-3, ソフトウェアサイエンス)
- J-050 NUIを用いた効果的なプレゼンテーションに関する研究(J分野:ヒューマンコミュニケーション&インタラクション,一般論文)