Specification and verification techniques of embedded systems using probabilistic linear hybrid automata

被引：0
作者：
Mutsuda, Y [1 ]
Kato, T [1 ]
Yamane, S [1 ]
机构：
[1] Kanazawa Univ, Grad Sch Nat Sci & Technol, Kanazawa, Ishikawa 9201192, Japan
来源：
EMBEDDED SOFTWARE AND SYSTEMS, PROCEEDINGS | 2005年 / 3820卷
关键词：
REAL-TIME SYSTEMS; MODEL CHECKING;
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We can model embedded systems as hybrid systems. Moreover, they are distributed and real-time systems. Therefore, it is important to specify and verify randomness and soft real-time properties. For the purpose of system verification, we formally define probabilistic linear hybrid automaton and its symbolic reachability analysis method. It can describe uncertainties and soft real-time characteristics. Our proposal method is the first attempt to symbolically verify probabilistic linear hybrid automata.
引用
收藏
页码：346 / 360
页数：15
相关论文
共 27 条
  • [1] Verification and Control of Probabilistic Rectangular Hybrid Automata
    Sproston, Jeremy
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 : 1 - 9
  • [2] A toolset for the specification and verification of embedded systems
    Rebaiaia, ML
    Benmohamed, M
    Jaam, JM
    Hasnah, A
    PDPTA'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS 1-4, 2003, : 1539 - 1545
  • [3] Verification and control for probabilistic hybrid automata with finite bisimulations
    Sproston, Jeremy
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 103 : 46 - 61
  • [4] Automated Verification Techniques for Probabilistic Systems
    Forejt, Vojtech
    Kwiatkowska, Marta
    Norman, Gethin
    Parker, David
    FORMAL METHODS FOR ETERNAL NETWORKED SOFTWARE SYSTEMS, SFM 2011, 2011, 6659 : 53 - 113
  • [5] Verifying Automata Specification ofDistributed Probabilistic Real-Time Systems
    罗铁庚
    陈火旺
    王兵山
    王戟
    龚正虎
    齐治昌
    JournalofComputerScienceandTechnology, 1998, (06) : 588 - 596
  • [6] Verifying automata specification of distributed probabilistic real-time systems
    Luo Tiegeng
    Chen Huowang
    Wang Bingshan
    Wang Ji
    Gong Zhenghu
    Qi Zhichang
    Journal of Computer Science and Technology, 1998, 13 (6) : 588 - 596
  • [7] Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates
    Huang, Chao
    Chen, Xin
    Lin, Wang
    Yang, Zhengfeng
    Li, Xuandong
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2017, 16
  • [8] Bounded Verification of Reachability of Probabilistic Hybrid Systems
    Lal, Ratan
    Prabhakar, Pavithra
    QUANTITATIVE EVALUATION OF SYSTEMS, QEST 2018, 2018, 11024 : 240 - 256
  • [9] A note on the verification of automata specifications of probabilistic real-time systems
    Moura, AV
    Pinto, GA
    INFORMATION PROCESSING LETTERS, 2002, 82 (05) : 223 - 228
  • [10] Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification
    Xie, Dingbao
    Bu, Lei
    Li, Xuandong
    2014 IEEE 35TH REAL-TIME SYSTEMS SYMPOSIUM (RTSS 2014), 2014, : 128 - 137
123