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 条

[21] Component-based system design: Analytic real-time interfaces for state-based component implementations [J].

Lampka K. ;

Perathoner S. ;

Thiele L. .

International Journal on Software Tools for Technology Transfer, 2013, 15 (3) :155-170

[22] Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems [J].

Muniz, Andre L. N. ;

Andrade, Aline M. S. ;

Lima, George .

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) :29-37

[23] Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets [J].

Nigro, Libero ;

Cicirelli, Franco .

MATHEMATICS, 2024, 12 (06)

[24] Conformance testing of real-time component based systems [J].

Tarhini, A ;

Fouchal, H .

ADVANCED DISTRIBUTED SYSTEMS, 2005, 3563 :167-181

[25] Modeling and verification of real-time embedded systems with urgency [J].

Hsiung, Pao-Ann ;

Lin, Shang-Wei ;

Chen, Yean-Ru ;

Huang, Chun-Hsian ;

Shih, Chihhsiong ;

Chu, William C. .

JOURNAL OF SYSTEMS AND SOFTWARE, 2009, 82 (10) :1627-1641

[26] Refinement-Based Verification of Interactive Real-Time Systems [J].

Spichkova, Maria .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 214 :131-157

[27] Communications-oriented development of component-based vehicular distributed real-time embedded systems [J].

Mubeen, Saad ;

Maki-Turja, Jukka ;

Sjodin, Mikael .

JOURNAL OF SYSTEMS ARCHITECTURE, 2014, 60 (02) :207-220

[28] Component-Based Modeling for Embedded Systems [J].

Chen, Fulong ;

Fan, Xiaoya ;

Wei, Jianjun .

2009 WASE INTERNATIONAL CONFERENCE ON INFORMATION ENGINEERING, ICIE 2009, VOL I, 2009, :414-+

[29] A Component-Based Approach for the Development of Automated Systems [J].

Mosbahi, Olfa ;

Khalgui, Mohamed ;

Hanish, Hans-Michael ;

Li, Zhiwu .

IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2011, 41 (05) :1026-1031

[30] Formal component-based modeling and synthesis for PLC systems [J].

Zhou, M. ;

Wan, H. ;

Wang, R. ;

Song, X. ;

Su, C. ;

Gu, M. ;

Sun, J. .

COMPUTERS IN INDUSTRY, 2013, 64 (08) :1022-1034

← 1 2 3 4 5 →