EMERALD: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems

被引：9

作者：

Zhang, Yizhou ^{[1
]}

Lin, Hao ^{[1
]}

Li, Guoqiang ^{[1
]}

机构：

[1] Shanghai Jiao Tong Univ, Sch Software, BASICS, Shanghai, Peoples R China

来源：

2012 12TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC) | 2012年

关键词：

Real-time systems; modeling; verification; controller automata; timed automata;

D O I：

10.1109/QSIC.2012.27

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Controller automata, extending timed automata, are a formal theory to model and analyze real-time systems with mutex components. Given a strict partial order over states, an ordered controller automaton can be faithfully translated into a timed automaton. We present a tool named EMERALD to translate ordered controller automata into timed automata and perform the transformation between their specifications in order to use the existing model checking engine, UPPAAL.

引用

页码：120 / 123

页数：4

共 50 条

[31] Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems [J].

Boudjadar, Abdeldjalil ;

Vaandrager, Frits ;

Bodeveix, Jean-Paul ;

Filali, Mamoun .

FUNDAMENTALS OF SOFTWARE ENGINEERING, FSEN 2013, 2013, 8161 :111-132

[32] Predicate Diagrams for the Verification of Real-Time Systems [J].

Kang, Eun-Young ;

Merz, Stephan .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 145 :151-165

[33] Compositional verification of embedded real-time systems [J].

Foughali, Mohammed ;

Hladik, Pierre-Emmanuel ;

Zuepke, Alexander .

JOURNAL OF SYSTEMS ARCHITECTURE, 2023, 142

[34] Verification of SimCo - Simulation Tool for Testing of Component-based Application [J].

Lipka, Richard ;

Potuzak, Tomas ;

Brada, Premysl ;

Herout, Pavel .

2013 IEEE EUROCON, 2013, :467-474

[35] Component-based specification, design and verification of adaptive systems [J].

Graics, Bence ;

Molnar, Vince ;

Majzik, Istvan .

SYSTEMS ENGINEERING, 2023, 26 (05) :567-589

[36] Component-Based Modeling and Verification of Dynamic Adaptation in Safety-Critical Embedded Systems [J].

Adler, Rasmus ;

Schaefer, Ina ;

Trapp, Mario ;

Poetzsch-Heffter, Arnd .

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 10 (02)

[37] MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS [J].

Li, Guoquiang ;

Cai, Xiaojuan ;

Yuen, Shoji .

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2012, 23 (04) :831-851

[38] Component-Based Formal Modeling of PLC Systems [J].

Wang, Rui ;

Guan, Yong ;

Luo Liming ;

Li, Xiaojuan ;

Zhang, Jie .

JOURNAL OF APPLIED MATHEMATICS, 2013,

[39] Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms [J].

Bersani, Marcello M. ;

Furia, Carlo A. ;

Pradella, Matteo ;

Rossi, Matteo .

SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2009, :13-+

[40] Component-Based Mixed-Criticality Real-Time Scheduling on a Single Processor System [J].

Ma, Dandi .

IEEE ACCESS, 2024, 12 :123208-123223

← 1 2 3 4 5 →