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 条

[21] Testing Real-Time Systems Using Determinization Techniques for Automata over Timed Domains
Krichen, Moez
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2019, 2019, 11884 : 124 - 133
[22] Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems
Damm, Werner
Pinto, Guilherme
Ratschan, Stefan
INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2007, 18 (01) : 63 - 86
[23] Specification and Validation of Embedded Systems using LUSTRE and ARGOS. Case Study: The Automatic Headlight Leveling System
Rainer Gmehlich
Design Automation for Embedded Systems, 2001, 6 : 151 - 175
[24] Specification and validation of embedded systems using LUSTRE and ARGOS. Case study: The automatic headlight leveling system
Gmehlich, R
DESIGN AUTOMATION FOR EMBEDDED SYSTEMS, 2001, 6 (02) : 151 - 175
[25] Improving the reliability of real-time embedded systems using innate immune techniques
Lay, Nicholas
Bate, Iain
EVOLUTIONARY INTELLIGENCE, 2008, 1 (02) : 113 - 132
[26] Safety verification of finite real-time nonlinear hybrid systems using enhanced group preserving scheme
Zhang, Hui
Wu, Jinzhao
Lu, Jianguang
Tang, Juan
CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS, 2016, 19 (04): : 2189 - 2199
[27] Real-Time Model Predictive Control for Battery-Supercapacitor Hybrid Energy Storage Systems Using Linear Parameter-Varying Models
Jia, Chao
Cui, Junwei
Qiao, Wei
Qu, Liyan
IEEE JOURNAL OF EMERGING AND SELECTED TOPICS IN POWER ELECTRONICS, 2023, 11 (01) : 251 - 263

← 1 2 3 →