入力値のみ保持する変数をもつEFSM群に対する動的性質の検証
スポンサーリンク
概要
- 論文の詳細を見る
本稿では, 複数のEFSMが特定の遷移でのみ互いに同期を取りながら遷移していくEFSMシステム(EFSM/int system)に対する記号モデル検査アルゴリズムについて述べる.このEFSM/intシステムは入力整数値を保持することだけができるレジスタを持ち, システム中の各EFSMはそのレジスタ値と現入力の線形制約の論理結合式による遷移条件にしたがって遷移する.また, 対象記号検査式として, どんな入力系列に対しても, 特定の制約状態とレジスタ値の線形制約の論理結合式で指定された状況へ到達可能か, などといったことが記述できる.このようなEFSM/intシステムに対し, 記号検査式の真偽が自動判定できるためのループ構造に関する十分条件を与え, そのもとでの真偽判定アルゴリズムを与える.この際, 各EFSMが同期する遷移ごとで遷移系列を区切ることにより, 状態爆発をなるべく起こさない工夫をしている.
- 2000-11-20
著者
-
平田 雅之
大阪大学大学院医学系研究科 神経機能制御外科学
-
平田 雅之
大阪大学大学院基礎工学研究科情報数理系専攻
-
岡野 浩三
大阪大学大学院情報科学研究科
-
谷口 健一
大阪大学大学院情報科学研究科
-
平田 雅之
大阪大学大学院
関連論文
- 合成開口脳磁図解析法のてんかん外科への応用
- 手術計画のための機能診断と外科解剖 : 前頭葉言語領野周辺
- 経頭蓋磁気刺激(TMS)による幻肢痛患者の運動野マッピング
- 高頻度反復的経頭蓋磁気刺激療法の除痛機序 : 電気生理学的検討
- O1-1 てんかん焦点診断におけるI-123 iomazenil SPECTとFDG-PETの比較(画像1,一般演題(口演),第42回日本てんかん学会)
- Strutsフレームワークにおけるメタモデルを用いた追跡可能性実現手法の提案(アスペクト指向・Web)
- 幻肢痛に対する大脳皮質刺激療法のメカニズム解析
- 侵襲型BMIの進歩 (特集 BMIとリハビリテーション)
- 反復的経頭蓋磁気刺激による難治性神経因性疼痛の治療
- 求心路遮断性疼痛に対する運動野刺激療法, 脊髄刺激療法による脳内活動変化
- 局所脳律動変化にもとづいた脳機能マッピングと脳機能再建への応用
- 脳卒中後疼痛に対する治療戦略 : 大脳運動野刺激療法と脊髄刺激療法の長期予後
- 皮質脳波を用いたbrain mappingとneural decoding(脳インタフェース(感覚応答など),脳インタフェースの技術と応用,一般)
- O2-43 てんかん焦点診断におけるI-123 iomazenil SPECT統計画像解析の有用性(画像2,一般演題(口演),てんかん制圧:新たなステージに向けて,第41回日本てんかん学会)
- 反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法
- 機能的大脳半球切除術
- 求心路遮断痛に対する大脳一次運動野刺激術
- 脳卒中後疼痛に対する脊髄電気刺激療法の有効性
- 開口合成法を用いたMEGによる言語関連領野の時空間・周波数解析
- 確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
- UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
- SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
- UML/OCLに記述された時間QoSの階層的検証手法の提案
- 確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
- SPINによるStrutsアプリケーションの動作検証を目的としたモデル生成手法の提案
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- てんかん治療への機能的アプローチ (てんかん原性)
- 在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
- 中枢性脳卒中後疼痛に対する反復経頭蓋磁気刺激療法の除痛機序
- 拡張時間オートマトン群による実時間システムの記述および検証
- 幻肢痛における大脳皮質再構築の経頭蓋磁気刺激, 脳磁図, 感覚誘発電位による検討
- 局所脳律動変化にもとづいた脳機能マッピングと脳機能再建への応用
- 上肢痙縮に対する selective musculocutaneous neurotomy の有用性
- 痙性斜頸に対する反復的経頭蓋磁気刺激療法(rTMS)の試み
- 脊髄由来の難治性疼痛に対する脳神経外科的治療
- 脳卒中後疼痛に対する治療戦略 : 大脳運動野刺激療法と脊髄刺激療法の長期予後
- 時間システムを対象とした到達可能性解析の高速化手法の提案
- 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
- OCLのJMLへの変換ツールの実装と評価
- OCLのJMLへの変換ツールの実装について
- 実時間システムを対象としたCEGARによる抽象洗練の並列化手法
- Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
- 上位設計におけるシステムの振る舞い検証技術(システム設計のための形式手法の基礎と応用)
- B-001 Javaに対するDaikonを用いたインバリアント自動生成のための汎用基盤ツール(ソフトウェア,一般論文)
- JMLを用いた在庫管理プログラムの設計とESC/Java2を用いた検証
- 制約指向に基づいたUMLモデルの不整合検出・解消手法の提案(ソフトウェア,フォーマルアプローチ論文)
- 時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,フォーマルアプローチ論文)
- Daikonの限定利用によるJavaメソッドの事後条件の自動導出
- UMLモデルに対するXPathとXMI-differenceを用いた不整合検出と解消
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- D-3-6 分散実時間アプリケーションのUML/OCL記述から時間オートマトンネットワークを用いた動作仕様記述への変換手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- 分散環境実時間アプリケーション開発支援のためのTimeliness QoS一貫性検証系および時間制御コード生成系の実装
- 関数型言語ML向け形式的検証支援システムの試作
- 関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
- D-3-8 分散環境における実時間アプリケーション動作仕様記述からのJavaコード自動導出手法の提案(D-3. ソフトウェアサイエンス)
- マルチメディアシステムにおけるTimeliness QoS一貫性検証と時間制御コード導出
- ペトリネットで記述された簡易ブラウザ型の組込みJavaプログラム動作仕様に対する実行方式の提案
- ワークフロー記述向きの時間付きカラーペトリネット
- 時間制約付きカラーペトリネットで記述されたワークフローからのスケジュール導出
- 時間制約を持つGUI制御部の仕様記述の一手法
- 凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
- 入力値のみ保持する変数をもつEFSM群に対する動的性質の検証
- CPU設計導入教育への形式的設計検証手法の適用
- 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
- 1G-6 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
- 複数時間オートマトンによる仕様記述と検証
- 組合わせ幾何を用いた有理数プレスブルガー文真偽判定アルゴリズムにおける投影操作の高速化
- 時間ペトリネットの拡張モデルを用いたプロトコル合成
- Tarski算術における冠頭標準形の閉論理式の真偽判定アルゴリズムの提案
- 耐故障性のための多重化リソースを持つ分散システムの導出法
- GUI制御部の記述と実現の一手法
- 規則右辺に照合外変数を含む条件付き項書換え系における階層合流性のモジュラ性
- 複数反例抽出を用いたCEGARによる時間オートマトンの抽象洗練手法
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (知能ソフトウェア工学)
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (ソフトウェアサイエンス)
- OCLからJMLへの変換ツールにおける対応クラスの拡張と教務システムに対する適用実験
- 4. ブレイン・マシン・インターフェースによる運動・言語機能再建(PS1-5 ニューロリハビリテーションの進歩,プレナリーセッション,脳神経外科医のProfessional SpiritとResearch Mind,第31回日本脳神経外科コングレス総会)
- 脳表電極を用いたブレイン・マシン・インタフェースの展望
- ブレイン・マシン・インタフェース用64chニューラルレコーディングチップ(アナログ,アナデジ混載,RF及びセンサインタフェース回路)
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価
- ブレイン・マシン・インターフェースによる運動・意思疎通機能再建のためのワイヤレス完全体内埋込装置の開発
- 経頭蓋磁気刺激による大脳運動野刺激療法の確立
- パーキンソン病に対する反復的経頭蓋磁気刺激療法(rTMS)の有効性の検討
- Local field potential から考えるパーキンソン病に対するSTN-DBSの展望
- 視床下核刺激療法(STN-DBS)が温冷覚に及ぼす影響についての検討
- 皮質脳波の生理学的特徴を用いて患者の訓練なく制御できるロボットハンドBMI
- 痙性対麻痺に対するバクロフェン髄腔内投与療法
- 神経疾患に対する非侵襲的中枢神経刺激療法 : 反復経頭蓋磁気刺激
- 4. ブレイン・マシン・インターフェースの最先端(PS1-4 機能外科と神経科学,プレナリーセッション,脳神経外科学の課題,第32回日本脳神経外科コングレス総会)
- シンポジウム 麻痺患者における感覚運動野皮質脳波の変化とBMIへの応用 (第16回認知神経科学会(その1))
- てんかん診療最前線 てんかん治療におけるbrain machine interfaceの可能性
- コミュニケーション ALSを対象としたブレイン・マシン・インターフェイス(BMI)の臨床応用への期待
- K-068 ブレイン・マシン・インターフェース(BMI)とリハビリテーション(先端科学と理学療法,特別講演III,プロフェッション!新たなるステージへ,第47回日本理学療法学術大会)
- ブレイン・マシン・インターフェースによる機能支援 : リアルタイムロボットアーム制御とワイヤレス完全体内埋込装置の開発(ニューロリハビリテーションの進歩)
- ニューラルレコーディングチップのデータ伝送方式(最先端の脳科学と集積化技術の融合)
- 神経領域の生理機能検査の現状と展開