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 条

[31] Formal Verification of Vessel Scheduling Using Probabilistic Timed Automata
Thianpunyathanakul, Ratchanok
Vatanawood, Wiwat
PROCEEDINGS OF THE 20TH INTERNATIONAL CONFERENCE ON COMPUTING AND INFORMATION TECHNOLOGY, IC2IT 2024, 2024, 973 : 65 - 72
[32] Using priced timed automata for the specification and verification of CSMA/CA in WSNs
Zohra H.
Kahloul L.
Benharzallah S.
International Journal of Information and Communication Technology, 2020, 17 (02) : 129 - 145
[33] Hybrid modeling and verification of embedded control systems
Mosterman, PJ
Biswas, G
Sztipanovits, J
COMPUTER AIDED CONTROL SYSTEMS DESIGN (CACSD'97), 1997, : 33 - 38
[34] 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
[35] Formal specification and verification method of concurrent and distributed systems by restricted timed automata
Yamane, S
TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 169 - 183
[36] Parameterized verification of linear networks using automata as invariants
Sistla, A. Prasad
Gyuris, Viktor
Formal Aspects of Computing, 11 (04): : 402 - 425
[37] Parametrized verification of linear networks using automata as invariants
Sistla, AP
COMPUTER AIDED VERIFICATION, 1997, 1254 : 412 - 423
[38] Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
Olveczky, Peter Csaba
Meseguer, Jose
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (36): : 137 - 157
[39] Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)
Broy, Manfred
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION, PROCEEDINGS, 2008, 17 : 1 - 13
[40] Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)
Broy, Manfred
Communications in Computer and Information Science, 2009, 17 : 1 - 13

← 1 2 3 4 5 →