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

閲覧可能ファイル 

ファイル	フォーマット	サイズ	閲覧回数	利用開始日	説明
itr102_616_013	pdf	705 KB	28	2014.04.11

論文情報

タイトル	拡張時間オートマトン群による実時間システムの記述および検証
	Specification and Verification of Real-Time System with Extended Timed Automata
	カクチョウ　ジカン　オートマトングン　ニ　ヨル　ジツジカン　システム　ノ　キジュツ　オヨビ　ケンショウ
著者	著者名 加藤, 雄一郎 カトウ, ユウイチロウ Kato, Yuichiro
	NRID 1000080314409 1000080314409 著者名 山口, 弘純 ヤマグチ, ヒロズミ Yamaguchi, Hirozumi
	NRID 1000070252632 1000070252632 著者名 岡野, 浩三 オカノ, コウゾウ Okano, Kozo
	NRID 1000000029513 1000000029513 著者名 谷口, 健一 タニグチ, ケンイチ 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
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27450
ISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2003 IEICE
	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

ホームへ戻る