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 条
  • [41] PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata
    Damm, Werner
    Ihlemann, Carsten
    Sofronie-Stokkermans, Viorica
    MATHEMATICS IN COMPUTER SCIENCE, 2011, 5 (04) : 469 - 497
  • [42] Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
    Damm, Werner
    Horbach, Matthias
    Sofronie-Stokkermans, Viorica
    FRONTIERS OF COMBINING SYSTEMS, FROCOS 2015, 2015, 9322 : 186 - 202
  • [43] 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
  • [44] Decidability and Complexity for the Verification of Safety Properties of Reasonable Linear Hybrid Automata
    Damm, Werner
    Ihlemann, Carsten
    Sofronie-Stokkermans, Viorica
    HSCC 11: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2011, : 73 - 82
  • [45] Adaptive techniques for specification matching in embedded systems: A comparative study
    Malik, R
    Roop, PS
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2005, 3771 : 33 - 52
  • [46] Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
    Adelt, Julius
    Mensing, Robert
    Herber, Paula
    FORMAL METHODS, PT II, FM 2024, 2025, 14934 : 208 - 228
  • [47] A SOC-Based Formal Specification and Verification of Hybrid Systems
    Yu, Ning
    Wirsing, Martin
    RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES (WADT 2014), 2015, 9463 : 151 - 169
  • [48] Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations
    Botchkarev, O
    Tripakis, S
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2000, 1790 : 73 - 88
  • [49] Loop reduction techniques for reachability analysis of linear hybrid automata
    Pan MinXue
    Li You
    Bu Lei
    Li XuanDong
    SCIENCE CHINA-INFORMATION SCIENCES, 2012, 55 (12) : 2663 - 2674
  • [50] Loop reduction techniques for reachability analysis of linear hybrid automata
    MinXue Pan
    You Li
    Lei Bu
    XuanDong Li
    Science China Information Sciences, 2012, 55 : 2663 - 2674
12345