SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察
スポンサーリンク
概要
- 論文の詳細を見る
近年,記号モデル検査の有効な手法として命題論理式の充足可能性問題(satisfiability,SAT)を利用する有界モデル検査が注目を集めている.データを含む分散システムの有界モデル検査手法において,SATソルバーではなくSMTソルバー(SAT modulo theories)を用いるとより効率的であることが知られている.また,我々はSOAに基づくシステムを設計・検証するためのUMLサブセットとして,cbUMLを提案した.よって本論文では,cbUMLにおける状態機械のSMTソルバーを用いる有界モデル検査手法を考察する.
- 2012-01-19
著者
関連論文
- モジュラーペトリネットを用いたマルチエージェントネットの可達性解析について(ペトリネット,離散事象システム,一般)
- ペトリネットを用いたコレオグラフィ実現について
- NGMS:次世代生産しシステム : 分散型生産・ビジネスモデルの協調的統合(Inteligent Manufacturing Systems:IMS)
- CSTソリューションコンペティション2007及び2008の総括(ペトリネット,離散事象システム,一般)
- AI-2-1 CSTソリューションコンペティション2008 : 総括(AI-2.CSTソリューションコンペティション2008:表彰式・シンポジウム,ソサイエティ企画)
- AK-2-3 マルチカーエレベータ群管理アルゴリズムに関する研究動向 : CSTソリューションコンペティション2007の活動を通じて(AK-2.基礎・境界分野の研究最前線,ソサイエティ特別企画,ソサイエティ企画)
- CSTソリューションコンペティション2007 : 評価実験の詳細報告(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- AI-1-5 CSTソリューションコンペティション2007(総括)(AI-1. CSTソリューションコンペティション2007:表彰式・シンポジウム,依頼シンポジウム,ソサイエティ企画)
- 需要家が複数存在する分散EMSにおける取引決定手法
- マルチエージェントネットの可達空間生成アルゴリズム(コンカレントシステム, 一般)
- シーケンス制御システムのマルチエージェントネットモデル導出手法
- A-12-4 マルチエージェントネットによる制御システムのモデル化(A-12. コンカレント工学)
- 分散EMSにおけるエネルギー取引決定手法の評価
- A-12-8 多期間における分散EMSの最適運転計画問題(A-12. コンカレント工学,一般セッション)
- A-12-3 拡張ROOM法における先行子表編集のためのGUIの開発(A-12. コンカレント工学,一般セッション)
- Safety Critical Systemに対する強化学習適用に関する検討(コンカレント工学一般、及び、CSTソリューションコンペティション2007発表会)
- MCEの群管理制御器:スケジュール完了時間の最適化とサービス範囲保証のためのパーキング戦略を適用したアルゴリズム(CSTコンペ・ソリューション発表,コンカレント工学一般、及び、CSTソリューションコンペティション2007発表会)
- 分散EMSにおけるエネルギー取引決定手法に対する市場指向プログラミングの適用
- 秘密分散共有法を用いた分散データベースシステムのマルチエージェントネットによる実現について(グラフ,ペトリネット,ニューラルネット及び一般)
- エージェントネットに基づくSOA検証用UMLシミュレータの提案(UML/開発方法論)
- A-12-10 複数市場が存在する分散EMSにおけるエネルギー取引決定手法の検討(A-12.コンカレント工学,一般講演)
- A-12-9 タブサーチを用いた自律分散型AGVの搬送計画手法(A-12.コンカレント工学,一般講演)
- CO_2排出量を考慮した分散EMSへの市場指向プログラミングの適用(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- 環境負荷を考慮したエネルギー取引システムシミュレータにおけるJavaクラスの開発(コンカレントシステム, 離散事象システム, ハイブリッドシステム, 及び一般)
- 環境負荷を考慮したエネルギー取引システムのシミュレータの開発
- SA-7-5 マルチエージェントによる環境負荷を考慮した分散EMSの最適運用に関する研究(SA-7. 企業・社会活動におけるコンカレント技術)
- マルチエージェントによる環境負荷を考慮した分散EMSの最適運用に関する研究
- AS-3-5 マルチカーエレベータの群制御問題への協調学習手法の適用(AS-3.コンカレントシステム理論の最近の発展とその応用,シンポジウムセッション)
- AS-3-4 CSTソリューションコンペティション2010の概要 : マルチカーエレベータの最適制御(AS-3.コンカレントシステム理論の最近の発展とその応用,シンポジウムセッション)
- A-12-3 UMLステートマシンの有界モデル検査における同期遷移の記号表現方法の一考察(A-12.コンカレント工学,一般セッション)
- A-12-1 UMLコミュニケーション図からUML状態機械図の自動生成をペトリネットの可達空間を展開せずに行う手法について(A-12.コンカレント工学,一般セッション)
- 秘密分散共有法を用いた分散データベースシステムの設計及び実装
- A-12-8 CSTソリューションコンペティション2007 : 課題と評価ツール(A-12.コンカレント工学,一般講演)
- 秘密分散共有法を用いた分散データベースシステムのマルチエージェントネットによる実現について(グラフ,ペトリネット,ニューラルネット及び一般)
- 第52回自動制御連合講演会
- アクティビティ図によるコレオグラフィ実現に関する研究(一般)
- Mariaを用いたマルチエージェントネットのモジュラー可達性解析(一般)
- ペトリネットを用いたコレオグラフィ実現について
- A-12-10 SCSDSPアルゴリズムのシャフト内のかご数増加に対する性能の評価及びアップピーク時におけるサービス完了時間の改善(A-12.コンカレント工学,一般セッション)
- MCEの群管理制御 : スケジュール完了時間の最適化,スケジュール方向の同期化及びパーキング戦略を適用したアルゴリズム(グラフ,ペトリネット,ニューラルネット,及び一般)
- A-12-2 Safety Critical Systemにおける強化学習の適用に関する一考察(A-12.コンカレント工学,一般講演)
- ペトリネットを用いたコミュニケーション図からステートマシン図の自動生成について(グラフ,ペトリネット,ニューラルネット,及び一般)
- MCEの群管理制御 : スケジュール完了時間の最適化,スケジュール方向の同期化及びパーキング戦略を適用したアルゴリズム(グラフ,ペトリネット,ニューラルネット,及び一般)
- ペトリネットを用いたコミュニケーション図からステートマシン図の自動生成について(グラフ,ペトリネット,ニューラルネット,及び一般)
- CSTソリューションコンペティション2007 : 評価ツールの詳細(グラフ,ペトリネット,ニューラルネット及び一般)
- CSTソリューションコンペティション2007 : 評価ツールの詳細(グラフ,ペトリネット,ニューラルネット及び一般)
- 自律分散ストレージシステムの自動修復機能の設計と実装(グラフ,ペトリ,ニューラルネット,及び一般)
- 自律分散ストレージシステムの自動修復機能の設計と実装(グラフ,ペトリ,ニューラルネット,及び一般)
- T-Tブリッジ除去によるUMLコミュニケーション図からUML状態機械図への変換手法について(グラフ,ペトリネット,ニューラルネット及び一般)
- T-Tブリッジ除去によるUMLコミュニケーション図からUML状態機械図への変換手法について(グラフ,べトリネット,ニューラルネット及び一般)
- 同期遷移と非同期遷移が混在するUML状態機械の有界モデル検査における記号表現方法の一考察(グラフ,ペトリネット,ニューラルネット及び一般)
- 同期遷移と非同期遷移が混在するUML状態機械の有界モデル検査における記号表現方法の一考察(グラフ,べトリネット,ニューラルネット及び一般)
- 秘密分散共有データベースにおける分散クエリ最適化問題について(コンカレントシステム,一般)
- マルチエージェントネットを用いた自律分散型FMSのコンカレント設計
- 自動倉庫システムのエージェント指向設計手法について
- A-12-4 BPEL/UML動作検証用シミュレータの研究(A-12.コンカレント工学,一般講演)
- Activity hypergraphを使用したBPEL4WS/UML記述のシミュレーション手法の提案(コンカレントシステム, 一般)
- Activity hypergraphを使用したBPEL4WS/UML記述のシミュレーション手法の提案
- フローショップ型生産システムの電気回路モデルと感度解析
- A-12-4 生産システムの電気回路モデルと感度解析
- CST2000-5 生産システムの電気回路モデルと感度解析
- A-12-2 自律分散ストレージシステムの信頼性向上手法の検討(A-12. コンカレント工学)
- マルチエージェントによる自律分散ストレージシステムの設計と実装(コンカレント工学一般)
- A-12-7 秘匿性・信頼性を保証したストレージシステムのためのエージェントの設計
- 交通信号システムの自律分散制御のためのマルチエージェントモデルについて(コンカレント工学及びハイブリッドダイナミカルシステムの理論と応用,一般)
- 秘匿性・信頼性を保証したストレージシステムのWebDAVフロントエンドの開発(コンカレント工学一般)
- マルチエージェントネットを用いたデマンドバスシミュレーションシステム
- 階層型マルチエージェントネットの通信機構について
- SA-7-9 マルチエージェントネットの分散シミュレーション
- SA-7-2 Peer to Peerコラボレーションソフトウェアのためのデータ同期・管理手法の提案(SA-7. 企業・社会活動におけるコンカレント技術)
- 秘密分散共有法を利用した自律分散ストレージシステム(情報セキュリティ応用)
- A-12-1 自律分散ストレージシステムのための代数体実現法の検討(A-12. コンカレント工学)
- A-12-8 秘匿性・信頼性を保証したストレージシステムの WebDAV フロントエンドについて
- A-12-1 秘密分散共有法を用いた分散データベースシステムに関する研究(A-12.コンカレント工学,一般講演)
- 遺伝的アルゴリズムを用いたラインバランシング手法について(コンカレント工学及びハイブリッドダイナミカルシステムの理論と応用,一般)
- 自律分散型AGVの搬送計画問題における初期割り当ての手法の評価(コンカレントシステム,一般)
- 自律分散型AGVの搬送計画問題における初期割り当ての手法の評価
- 搬送経路計画問題における初期割り当て手法に関する研究(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- A-12-3 自律分散型AGVの搬送計画問題における計算時間短縮法の提案(A-12.コンカレント工学,一般講演)
- 「システム設計のための形式手法の基礎と応用」特集号を企画して
- 分岐限定法を用いた単一製品フローショップの生産資源計画
- SA-6-3 単一製品フローショップの生産システム計画に対するコンカレント手法
- CO2排出量を考慮したエネルギー取引システムに関する一考察
- A-12-6 生産システムのバッファ使用量に注目した状況依存エージェントの設計
- C02排出量を考慮した分散EMSの多期間問題への拡張
- 秘密分散共有法を用いた分散データベースシステムにおける縦分割アルゴリズム(グラフ, ペトリ, ニューラルネット及び一般)
- A-12-2 秘密分散データベースシステムにおける離接クエリの最適化(A-12. コンカレント工学, 基礎・境界)
- A-12-1 分散EMSの最適運転計画ソフトウェアに関する研究(A-12. コンカレント工学, 基礎・境界)
- A-12-7 探索技法を用いる自律分散エージェントによるデマンドバスシステムの乗客獲得手法
- A-12-6 デマンドバス問題におけるエージェント間交渉を用いた運行計画手法
- シェア配送問題に対する発見的手法の比較(グラフ,ペトリ,ニューラルネット及び一般)
- シェア配送問題に対する発見的手法の比較(グラフ,ペトリ,ニューラルネット及び一般)
- シェア配送問題に対する発見的手法の比較
- 秘密分散ストレージシステムにおける最適シェア配送問題(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- CSTソリューションコンペティション2010 : マルチカーエレベータの最適制御(CSTソリューションコンペティション2010,コンカレントシステム及び一般)
- CO_2排出量を考慮した分散EMSの多期間問題への拡張
- システム・情報部門学術講演会(SICE-SSI2005)
- A-3-5 コンカレント生産資源計画システムにおける資源レイアウト機能の拡張
- POMDPs環境における状態遷移の部分的履歴を用いた強化学習法(研究速報)
- AS-3-5 ペトリネットを用いたサービス振る舞いモデルの自動合成(AS-3.ワークフローとビジネスプロセス管理への数理的アプローチ,シンポジウムセッション)