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

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

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2003, 102(616), 13-18

Number of Access:897（2025-08-15 06:46 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27450

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr102_616_013 pdf None 705 KB 75 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
拡張時間オートマトン群による実時間システムの記述および検証
Specification and Verification of Real-Time System with Extended Timed Automata
カクチョウ　ジカン　オートマトングン　ニ　ヨル　ジツジカン　システム　ノ　キジュツ　オヨビ　ケンショウ
Creator
CreatorName
加藤, 雄一郎 ; カトウ, ユウイチロウ ; Kato, Yuichiro
NRID
1000080314409 1000080314409
ORCID
0000-0003-2273-4876 0000-0003-2273-4876
researchmap permalink
hirozumi.yamaguchi hirozumi.yamaguchi
Scopus Author ID
7404274201 7404274201
CreatorName
山口, 弘純 ; ヤマグチ, ヒロズミ ; Yamaguchi, Hirozumi
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000000029513 1000000029513
CreatorName
谷口, 健一 ; タニグチ, ケンイチ ; Taniguchi, Kenichi
Subject
実時間システム
時間オートマトン
検証
real-time system
timed automaton
verification
Abstract
この論文では, 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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
102(616)
Page
13-18
Date of Issued
2003-01-23
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27450
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2003 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article