拡張時間オートマトン群による実時間システムの記述および検証  [in Japanese] Specification and Verification of Real-Time System with Extended Timed Automata  [in Japanese]

Access this Article

Search this Article

Author(s)

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.

Journal

  • Technical report of IEICE. SS

    Technical report of IEICE. SS 102(616), 13-18, 2003-01-23

    The Institute of Electronics, Information and Communication Engineers

References:  4

Codes

  • NII Article ID (NAID)
    110003276632
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    6467551
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS  IR 
Page Top