検索結果を絞り込む

データ種別

論文 47 博士論文 1

本文・本体へのリンク

本文・本体リンクあり 47

〜

検索結果 47 件

  • 1 / 1

  • IoT Modeling and Verification: From the CaIT Calculus to UPPAAL

    CHEN Ningning, ZHU Huibiao IEICE Transactions on Information and Systems E106.D (9), 1507-1518, 2023-09-01

    ...To support the use of UPPAAL to verify the temporal properties of IoT networks described by the CaIT calculus, we establish a relationship between timed automata and the CaIT calculus....

    DOI Web Site 参考文献28件

  • 要求分析段階におけるモデル検査技術を用いた設計制約検証の自動化

    池田, 彩恵, 松浦, 佐江子 第80回全国大会講演論文集 2018 (1), 211-212, 2018-03-13

    ...複数機器間での通信によりサービスを提供する複合システムのワークフローは,UMLモデルで定義することができる.しかし,UMLは,通信発生のタイミングや通信時間という設計制約の明示的な記述要素が無い.サブシステムは並列動作するため,設計制約により各サブシステムが取り得る膨大な数の状態から機器が同期しない状態を人の目で確認することは困難である.そこで,UMLモデルのフロー,シグナル送受信をモデル検査UPPAAL...

    情報処理学会

  • オブジェクト指向ペトリネットによる業務プロセスモデリングと時間制約の検証

    秦, 良平, 飯島, 正 ソフトウェアエンジニアリングシンポジウム2015論文集 2015 99-106, 2015-08-31

    ...Management) は，業務プロセス管理 (BPM; Business Process Management) の効率化に有効である．業務ルールの中でも，「時間制約に関するルール」は重要な要素の一つであり，本研究では，業務プロセスにおいて「時間制約に関するルール」をモデル検査手法を用いて検証することを目指す．著者らが提案する業務プロセス表記法に対して，時間表現を導入し，時間制約を含めたモデル検査ツールUPPAAL...

    情報処理学会

  • 組み込みシステムにおける設計制約を検証するためのUMLモデル検査手法

    小林, 雅弥, 松浦, 佐江子 第77回全国大会講演論文集 2015 (1), 361-362, 2015-03-17

    ...そこでワークフローに設計制約を表現するステレオタイプやタグ付き値を与え、モデル検査ツールUPPAALのモデルに変換して安全性、活性を検査し、検査結果をワークフローにフィードバックする方法を提案する。本稿では複数ロボットが協調する荷物の自動搬送システムへの適応事例により、その有効性を示す。...

    情報処理学会

  • クラウドにおけるデータ整合性評価

    西田 紗知, 新川 芳行 経営情報学会　全国研究発表大会要旨集 2015f (0), 176-179, 2015

    ...モデリングおよびシミュレーションには時間オートマトンに基づく検証ツールのUPPAALを用い、時相論理式の一種であるTCTLによりデータ整合性の検証・評価を行う。...

    DOI

  • モデル検査ツールを利用したリアクティブシステムのソフトウェアテスト

    田辺 誠 産業応用工学会全国大会講演論文集 2015 (0), 42-43, 2015

    ...本稿では、Web上のチケット予約システムを例として、モデル検査ツールUPPAALによるトレース解析を応用したテストケースの自動生成手法を提案する。 この手法により、モデルを解析してシステムが特定の状態に到達するまでの最短手順をテストケースとして導出することが出来、システムの効率的な開発につながる。...

    DOI

  • オブジェクト指向ペトリネットに基づくビジネスプロセスの時間制約に関するモデル検査

    秦 良平, 飯島 正 情報システム学会　全国大会論文集 11 (0), c21-, 2015

    ...業務プロセス管理において、時間制約の概念は重要な要素の一つである．著者らは，オブジェクト指向ペトリネットというモデルにより業務プロセスを記述し，そのモデルに時間表現を導入し拡張することに試みている．ここでは，時間表現を導入したオブジェクト指向ペトリネットを時間オートマトンに変換し，UPPAAL というモデル検査ツールを利用して，業務プロセスにおける時間制約をモデル検査手法を用いて検証する試みについて...

    DOI

  • ビジネスプロセスとビジネスルールのためのモデル検査手法による検証

    秦 良平, 小形 達也, 飯島 正 情報システム学会　全国大会論文集 10 (0), c21-, 2014

    ...近年，業務プロセス管理(BPM; Business Process Management) と並んで，業務ルール管理(BRM; Business Rule Management) が重視されている．本研究は，業務プロセスにおいて「時間制約に関する業務ルール」をモデ ル検査手法を用いて検証することを目指すものである．モデル検査には，時間に関する検証を行うツールUPPAAL を採用する．著者らの提案する...

    DOI

  • 実時間システム向け文脈指向言語ProcneJ

    安原, 由貴, 森口, 草介, 渡部, 卓雄 情報処理学会論文誌プログラミング（PRO） 6 (3), 50-50, 2013-12-20

    組込みシステム等において典型的に要求される性質に実時間制約がある．実時間制約は横断的関心事の1つであり，プログラムを複雑にする．本研究の目的は，文脈指向プログラミングの考え方に基づいた実時間制約の記述方式とそのモジュール化手法，およびそれに基づくプログラミング言語の提案である．実時間システムのプログラムは，外部環境などの変化に加え，時刻および時間経過に依存する振舞いを示すプログラムと考えることが…

    機関リポジトリ 情報処理学会

  • 実時間システム向け文脈指向言語ProcneJ

    安原 由貴, 森口 草介, 渡部 卓雄 情報処理学会論文誌プログラミング（PRO） 6 (3), 50-50, 2013-12-20

    ...In addition, by generating timed automata from the state transition parts, we can verify the consistency of real-time constraints using UPPAAL model checker....

    情報処理学会

  • 確率線形ハイブリッドオートマトンの到達可能性検証

    畠中, 克也, 山根, 智 情報処理学会論文誌 53 (12), 2671-2681, 2012-12-15

    ...リアルタイムシステムに対するモデル検査の需要は増加しており，時間オートマトンで記述したモデルを検証可能なUPPAALに代表される検証器の開発がさかんに行われている．本研究では，コスト付き確率時間オートマトンのモデル検査のprocedureを拡張し，確率線形ハイブリッドオートマトンに対する検証を可能にする．さらに，モデルに対する検証を自動化するため，拡張したprocedureを計算機上に実装する．ケーススタディ...

    情報処理学会 Web Site

  • UML要求分析モデルにおけるCRUD観点のデータライフサイクルの妥当性検査手法

    青木善貴, 小形真平, 奥田博隆, 松浦佐江子 第74回全国大会講演論文集 2012 (1), 239-240, 2012-03-06

    ...検査の網羅性・効率性・正確性を向上する1つの有益な技術としてモデル検査技術があるが，仕様が固定化しづらい要求分析への適用は難しいとされてきた．そこで，本稿では，これまで提案してきた顧客の妥当性確認を支援するプロトタイプ生成可能なUML要求分析モデルを対象に，モデル検査ツールUPPAALを活用したデータライフサイクルの網羅的かつ効率的な検査手法を提案する．...

    情報処理学会

  • 組み込みソフトウェア開発におけるハードウェア要件の分析と検証

    岡田康治, 松浦佐江子 第74回全国大会講演論文集 2012 (1), 391-392, 2012-03-06

    ...本稿では、要求分析段階で明らかにすべき様々な制約の内、機能的制約と時間制約をUMLクラス図、アクティビティ図で、それらの制約がソフトウェアの満たすべき目的のどの部分を満たすかをSysML要求図で分析し、UPPAALを用いてその妥当性を検査する手法を提案する。また、列車の運行制御の例題へ本手法を適用した結果を元に、有効性について議論する。...

    情報処理学会

  • 組み込みソフトウェア開発におけるハードウェア要件の分析と検証

    岡田康治, 松浦佐江子 第74回全国大会講演論文集 2012 (1), 391-392, 2012-03-06

    ...本稿では、要求分析段階で明らかにすべき様々な制約の内、機能的制約と時間制約をUMLクラス図、アクティビティ図で、それらの制約がソフトウェアの満たすべき目的のどの部分を満たすかをSysML要求図で分析し、UPPAALを用いてその妥当性を検査する手法を提案する。また、列車の運行制御の例題へ本手法を適用した結果を元に、有効性について議論する。...

    情報処理学会

  • UML要求分析モデルにおけるCRUD観点のデータライフサイクルの妥当性検査手法

    青木善貴, 小形真平, 奥田博隆, 松浦佐江子 第74回全国大会講演論文集 2012 (1), 239-240, 2012-03-06

    ...検査の網羅性・効率性・正確性を向上する1つの有益な技術としてモデル検査技術があるが，仕様が固定化しづらい要求分析への適用は難しいとされてきた．そこで，本稿では，これまで提案してきた顧客の妥当性確認を支援するプロトタイプ生成可能なUML要求分析モデルを対象に，モデル検査ツールUPPAALを活用したデータライフサイクルの網羅的かつ効率的な検査手法を提案する．...

    情報処理学会

  • 時間オートマトンによるフェースディスプレイの上位設計と形式的検証

    田川, 聖治, 高橋, 佑輔, 加藤, 暢 情報処理学会論文誌数理モデル化と応用（TOM） 3 (3), 44-53, 2010-10-25

    本稿では，フェースディスプレイの設計と検証の手法を提案している．フェースディスプレイとは，対象システムに同期して表情アニメーションを実行するものである．まず，フェースディスプレイのモデルは感性モデルと表現モデルの 2 階層により構成される．感性モデルは人間の心理状態の変化を記述し，表現モデルは人間の表情の変化を記述している．また，感性モデルと表現モデルは，それぞれ時間オートマトンにより定義してい…

    情報処理学会 Web Site

  • Verification of Flexray Start-Up Mechanism by Timed Automata

    Jan Malinský, Jiří Novák Metrology and Measurement Systems 17 (3), 461-480, 2010-01-01

    ...For this purpose the UPPAAL software tool has been used that allows the modelling of discrete event systems with the use of timed automata, and subsequently the verification of the model with the use of...

    DOI PDF XML 被引用文献1件

  • UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法

    長岡, 武志, 岡野, 浩三, 楠本, 真二 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 107 (176), 77-82, 2007-07-26

    近年,情報システムの高信頼設計においてモデル検査は重要な役割を果たすようになってきている.実時間システムのモデル検査では,モデルの状態数が状態変数やクロック変数に対して指数的に増加し,スケーラビリティに厳しい制限が生じる.本稿では,時間モデル検査ツールであるUPPAALで用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案する.モデル抽象化技法はこのスケーラビリティ改善のための主…

    HANDLE Web Site 被引用文献1件 参考文献8件

  • UML/OCLに記述された時間 QoS の階層的検証手法の提案

    長井, 栄吾, 岡野, 浩三, 楠本, 真二 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 106 (202), 13-18, 2006-07-28

    分散実時間アプリケーションにおいては,ユーザに対して提供されるQoS(Quality of Service)を保証することがきわめて重要である.特に,時間QoSに対する要求の保証が重要視されている.本稿では,UML/OCLに記述された時間QoSを多段階かつ階層的に検証する方法を提案する.コンポーネントの時間的振る舞いを時間オートマントで抽象化した抽象QoSモデルを利用することで,時間QoSを多段…

    HANDLE Web Site 被引用文献1件 参考文献9件

  • A Tutorial on Uppaal

    Gerd Behrmann, Alexandre David, Kim G. Larsen Lecture Notes in Computer Science 3185 200-236, 2004

    DOI PDF 被引用文献7件

  • 拡張時間オートマトン群による実時間システムの記述および検証

    加藤, 雄一郎, 山口, 弘純, 岡野, 浩三, 谷口, 健一 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 102 (616), 13-18, 2003-01-23

    この論文では, QoS制御機能をもった動画像再生システムを例に,拡張時問オートマトン群による実時間システムの記述及び検証について述べる.動画像再生システムの記述に検証のための追加や変更を行い,ジッターやフレーム再生間隔といったいくつかの性質をCTLで記述した.そして,チェッカーUppaalを用いて,記述した動画像再生システムが安全性と上記の性質を満たすかの検証を行った.また, …

    HANDLE Web Site 被引用文献1件 参考文献4件

  • Uppaal in a nutshell

    Kim G. Larsen, Paul Pettersson, Wang Yi International Journal on Software Tools for Technology Transfer 1 (1-2), 134-152, 1997-12

    DOI PDF Web Site ほか1件 被引用文献15件

  • 1 / 1
ページトップへ