ログイン 新規登録
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

  1. 全国大会
  2. 78回
  3. ソフトウェア科学・工学

ペトリネット検証ツールHiPSにおけるLTL仕様に基づいたOn-the-fly/Fluentモデル検査

https://ipsj.ixsq.nii.ac.jp/records/161699
https://ipsj.ixsq.nii.ac.jp/records/161699
434df412-df96-4099-9dca-da8a58e860e8
名前 / ファイル ライセンス アクション
IPSJ-Z78-3K-04.pdf IPSJ-Z78-3K-04.pdf (269.4 kB)
Copyright (c) 2016 by the Information Processing Society of Japan
オープンアクセス
Item type National Convention(1)
公開日 2016-03-10
タイトル
タイトル ペトリネット検証ツールHiPSにおけるLTL仕様に基づいたOn-the-fly/Fluentモデル検査
言語
言語 jpn
キーワード
主題Scheme Other
主題 ソフトウェア科学・工学
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_5794
資源タイプ conference paper
著者所属
信州大
著者所属
信州大
著者名 張江, 洋次朗

× 張江, 洋次朗

張江, 洋次朗

Search repository
和崎, 克己

× 和崎, 克己

和崎, 克己

Search repository
論文抄録
内容記述タイプ Other
内容記述 本稿では,ペトリネットより生成される状態空間を対象に,LTL式によるon-the-flyモデル検査器の設計について記す.筆者らの研究グループによって開発・公開されているペトリネット設計・検証ツールHiPSがある.HiPSでは,発火系列により構成される,ペトリネットの初期マーキングを根とするプロセス木を生成する機能が備わっている.HiPSは外部ツールと連携することで,状態空間に対するモデル検査を行うことができる.現状ではモデル検査を適用するためには全ての状態空間の生成を行わなくてはならず,時間的制約から大規模モデルへの適用は難しい.今回,モデル検査の効率化のため,on-the-fly手法を用いたLTLモデル検査器のHiPSツールへの組み込みを行った.
書誌レコードID
収録物識別子タイプ NCID
収録物識別子 AN00349328
書誌情報 第78回全国大会講演論文集

巻 2016, 号 1, p. 455-456, 発行日 2016-03-10
出版者
言語 ja
出版者 情報処理学会
戻る
0
views
See details
Views

Versions

Ver.1 2025-01-20 11:51:38.052893
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3