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
相关论文
共 50 条
  • [21] Application of Contract-based verification techniques for Hybrid Automata to Surgical Robotic Systems
    Schreiter, Luzie
    Bresolin, Davide
    Capiluppi, Marta
    Raczkowsky, Joerg
    Fiorini, Paolo
    Woern, Heinz
    2014 EUROPEAN CONTROL CONFERENCE (ECC), 2014, : 2310 - 2315
  • [22] Verification Techniques for Hybrid Systems
    Prabhakar, Pavithra
    Soto, Miriam Garcia
    Lal, Ratan
    LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, 9953 : 833 - 842
  • [23] 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
  • [24] Verifying Automata Specification ofDistributed Probabilistic Real-Time Systems
    罗铁庚
    陈火旺
    王兵山
    王戟
    龚正虎
    齐治昌
    JournalofComputerScienceandTechnology, 1998, (06) : 588 - 596
  • [25] 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
  • [26] Specification and Verification of Linear Dynamical Systems: Advances and Challenges
    Ouaknine, Joel
    FRONTIERS OF COMBINING SYSTEMS (FROCOS 2013), 2013, 8152 : 197 - 197
  • [27] Bounded Verification of Reachability of Probabilistic Hybrid Systems
    Lal, Ratan
    Prabhakar, Pavithra
    QUANTITATIVE EVALUATION OF SYSTEMS, QEST 2018, 2018, 11024 : 240 - 256
  • [28] Verification of linear hybrid automata by periodical properties on control states
    Pan, Guoqiang
    Yu, Huiqun
    Song, Guoxin
    Shao, Zhiqing
    Huadong Ligong Daxue Xuebao /Journal of East China University of Science and Technology, 2000, 26 (05): : 471 - 476
  • [29] Compositional specification and structured verification of hybrid systems in cTLA
    Herrmann, P
    Graw, G
    Krumm, H
    FIRST INTERNATIONAL SYMPOSIUM ON OBJECT-ORIENTED REAL-TIME DISTRIBUTED COMPUTING (ISORC '98), 1998, : 335 - 340
  • [30] Computational techniques for the verification of hybrid systems
    Tomlin, CJ
    Mitchell, I
    Bayen, AM
    Oishi, M
    PROCEEDINGS OF THE IEEE, 2003, 91 (07) : 986 - 1001
12345