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 条

[1] Verification using counterexample fragment based specification relaxation: Case of modular/concurrent linear hybrid automata
Ren, Hao (ren@iastate.edu), 2017, Institution of Engineering and Technology, United States (02):
[2] Verification and Control of Probabilistic Rectangular Hybrid Automata
Sproston, Jeremy
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 : 1 - 9
[3] 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
[4] Embedded systems: Challenges in specification and verification
Pnueli, A
EMBEDDED SOFTWARE, PROCEEDINGS, 2002, 2491 : 1 - 14
[5] Specification of Embedded Control Systems Behaviour Using Actor Interface Automata
Angelo, Christo
Zhou, Feng
Sierszecki, Krzysztof
SOFTWARE TECHNOLOGIES FOR EMBEDDED AND UBIQUITOUS SYSTEMS, 2010, 6399 : 167 - 178
[6] Modelling and verification using linear hybrid automata -: A case study
Müller, O
Stauner, T
MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS, 2000, 6 (01) : 71 - 89
[7] Formal verification of the MetaH executive using linear hybrid automata
Vestal, S
SIXTH IEEE REAL-TIME TECHNOLOGY AND APPLICATIONS SYMPOSIUM, PROCEEDINGS, 2000, : 134 - 144
[8] FORMAL TECHNIQUES FOR SYSTEMS SPECIFICATION AND VERIFICATION
CARMO, J
SERNADAS, A
INFORMATION SYSTEMS, 1991, 16 (03) : 245 - 272
[9] Verification and control for probabilistic hybrid automata with finite bisimulations
Sproston, Jeremy
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 103 : 46 - 61
[10] HieroMate: A Graphical Tool for Specification and Verification of Hierarchical Hybrid Automata
Mohammed, Ammar
Schwarz, Christian
KI 2009: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2009, 5803 : 695 - 702

← 1 2 3 4 5 →