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 条
[41]   Towards a Component-based Requirements Modeling for Automotive Systems [J].
Yan, Xuqin ;
Liu, Xiaojian ;
Wang, Zhixue ;
Che, Xiaobo ;
Mao, Chengyong ;
Li, Yang ;
Cheng, Wei .
ADVANCES IN SCIENCE AND ENGINEERING, PTS 1 AND 2, 2011, 40-41 :955-960
[42]   A Component-Based Modeling and Validation Method for PLC Systems [J].
Wang, Rui ;
Guan, Yong ;
Zhou, Min ;
Zhang, Jie ;
Song, Xiaoyu .
ADVANCES IN MECHANICAL ENGINEERING, 2014,
[43]   A Verification Tool for Real-Time Task Schedulability Analysis [J].
Nxumalo, Madoda ;
Timm, Nils ;
Gruner, Stefan .
SOUTH AFRICAN INSTITUTE OF COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS, SAICSIT 2023, 2023, 1878 :48-60
[44]   Formal verification of component-based designs [J].
Daniel Karlsson ;
Petru Eles ;
Zebo Peng .
Design Automation for Embedded Systems, 2007, 11 :49-90
[45]   Formal verification of component-based designs [J].
Karlsson, Daniel ;
Eles, Petru ;
Peng, Zebo .
DESIGN AUTOMATION FOR EMBEDDED SYSTEMS, 2007, 11 (01) :49-90
[46]   Procedure-Level Verification of Real-time Concurrent Systems [J].
Farn Wang ;
Chia-Tien Lo .
Real-Time Systems, 1999, 16 :81-114
[47]   Diagram-Based Verification of Real-Time Systems using Timed Predicate Diagrams [J].
Nugraheni, Cecilia E. .
INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2006, 6 (12) :18-27
[48]   Procedure-level verification of real-time concurrent systems [J].
Wang, F ;
Lo, CT .
REAL-TIME SYSTEMS, 1999, 16 (01) :81-114
[49]   A note on the verification of automata specifications of probabilistic real-time systems [J].
Moura, AV ;
Pinto, GA .
INFORMATION PROCESSING LETTERS, 2002, 82 (05) :223-228
[50]   Efficient verification of parallel real-time systems [J].
Yoneda, T ;
Schlingloff, BH .
FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) :187-215
12345