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

加藤, 雄一郎; 山口, 弘純; 岡野, 浩三; 谷口, 健一

このアイテムのアクセス数:77件（2021-01-19 18:48 集計）

このアイテムへのリンクには次のURLをご利用ください:http://hdl.handle.net/11094/27450

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr102_616_013	pdf	705 KB	22

論文情報

タイトル	拡張時間オートマトン群による実時間システムの記述および検証
別タイトル	Specification and Verification of Real-Time System with Extended Timed Automata
タイトル (ヨミ)	カクチョウ　ジカン　オートマトングン　ニ　ヨル　ジツジカン　システム　ノ　キジュツ　オヨビ　ケンショウ
著者	加藤, 雄一郎加藤, 雄一郎
	山口, 弘純山口, 弘純
	岡野, 浩三岡野, 浩三
	谷口, 健一谷口, 健一
著者の別表記	Kato, Yuichiro
	Yamaguchi, Hirozumi
	Okano, Kozo
	Taniguchi, Kenichi
著者 (ヨミ)	カトウ, ユウイチロウ
	ヤマグチ, ヒロズミ
	オカノ, コウゾウ
	タニグチ, ケンイチ
キーワード等	実時間システム
	時間オートマトン
	検証
	real-time system
	timed automaton
	verification
抄録	この論文では, QoS制御機能をもった動画像再生システムを例に,拡張時問オートマトン群による実時間システムの記述及び検証について述べる.動画像再生システムの記述に検証のための追加や変更を行い,ジッターやフレーム再生間隔といったいくつかの性質をCTLで記述した.そして,チェッカーUppaalを用いて,記述した動画像再生システムが安全性と上記の性質を満たすかの検証を行った.また, QoS制御機能のUppaalによる検証についても触れる.
抄録	In this paper, we present specification and verification examples of a real-time svstem (a video player with QoS controller) modeled in networks of (extended) timed automata, where they communicate via channels and global variables. We described sevearl properties, such as frame rate and jitter in CTL and test timed automata. We have verified that the player satisfies safety and those properties using Uppaal. We also discuss verification of QoS properties using Uppaal.
公開者	電子情報通信学会
公開者の別表記	The Institute of Electronics, Information and Communication Engineers
公開者 (ヨミ)	デンシ　ジョウホウ　ツウシン　ガッカイ
掲載誌名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻	102
号	616
開始ページ	13
終了ページ	18
刊行年月	2003-01-23
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27450
権利情報	Copyright © 2003 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.102(616) P.13-P.18
DC.title	拡張時間オートマトン群による実時間システムの記述および検証
DCTERMS.alternative	Specification and Verification of Real-Time System with Extended Timed Automata
DC.creator	加藤, 雄一郎
	山口, 弘純
	岡野, 浩三
	谷口, 健一
DC.creator	Kato, Yuichiro
	Yamaguchi, Hirozumi
	Okano, Kozo
	Taniguchi, Kenichi
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2003-01-23
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27450
DC.subject	実時間システム
	時間オートマトン
	検証
	real-time system
	timed automaton
	verification
DCTERMS.abstract	この論文では, QoS制御機能をもった動画像再生システムを例に,拡張時問オートマトン群による実時間システムの記述及び検証について述べる.動画像再生システムの記述に検証のための追加や変更を行い,ジッターやフレーム再生間隔といったいくつかの性質をCTLで記述した.そして,チェッカーUppaalを用いて,記述した動画像再生システムが安全性と上記の性質を満たすかの検証を行った.また, QoS制御機能のUppaalによる検証についても触れる.
DCTERMS.abstract	In this paper, we present specification and verification examples of a real-time svstem (a video player with QoS controller) modeled in networks of (extended) timed automata, where they communicate via channels and global variables. We described sevearl properties, such as frame rate and jitter in CTL and test timed automata. We have verified that the player satisfies safety and those properties using Uppaal. We also discuss verification of QoS properties using Uppaal.
DC.rights	Copyright © 2003 IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	拡張時間オートマトン群による実時間システムの記述および検証
citation_author	加藤, 雄一郎
	山口, 弘純
	岡野, 浩三
	谷口, 健一
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2003-01-23
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	102
citation_issue	616
citation_firstpage	13
citation_lastpage	18
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27450
citation_keywords	実時間システム
	時間オートマトン
	検証
	real-time system
	timed automaton
	verification

閲覧可能ファイル

論文情報

論文詳細を表示