STATE - a SystemC to Timed Automata Transformation Engine

被引：5

作者：

Herber, Paula ^{[1
]}

Pockrandt, Marcel ^{[1
]}

Glesner, Sabine ^{[1
]}

机构：

[1] Tech Univ Berlin, Ernst Reuter Pl 7, D-10587 Berlin, Germany

来源：

2015 IEEE 17TH INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING AND COMMUNICATIONS, 2015 IEEE 7TH INTERNATIONAL SYMPOSIUM ON CYBERSPACE SAFETY AND SECURITY, AND 2015 IEEE 12TH INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE AND SYSTEMS (ICESS) | 2015年

关键词：

HW/SW Co-Design; Timed Automata; Model Checking;

D O I：

10.1109/HPCC-CSS-ICESS.2015.188

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

SystemC is a system level design language that is widely used in hardware/software codesign. As the semantics of SystemC is only informally defined, verification of SystemC designs is mainly done using simulation and testing. With that, faults can be detected but it is impossible to verify the correctness of a given system for all possible executions. In this paper, we present our SystemC to Timed Automata Transformation Engine. STATE takes a SystemC design as input and transforms it into a UPPAAL timed automata model. This enables automated formal verification of SystemC designs using the UPPAAL model checker. To ease debugging, the transformation keeps the structure of the original SystemC design transparent to the designer in the resulting UPPAAL model. The current version of STATE supports many relevant SystemC language elements, including complex interactions between processes, dynamic sensitivity and timing behavior, structs, arrays, pointers, as well as the TLM 2.0 standard. We demonstrate the practical applicability of STATE with three case studies, including an industrial design of an AMBA bus.

引用

页码：1074 / 1077

页数：4

共 14 条

[1]

Behrmann G, 2004, LECT NOTES COMPUT SC, V3185, P200

[2] Software Model Checking SystemC [J].

Cimatti, Alessandro ;

Narasamdya, Iman ;

Roveri, Marco .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2013, 32 (05) :774-787

[3]

FZI Research Center for Information Technology, KASCPAR KARLSR SYSTE

[4]

Garavel H., 2009, MEMOCODE

[5]

Groae D., 2010, MEMOCODE

[6]

Habibi A., 2006, Design, Automation and Test in Europe, P76, DOI [10.1109/DATE.2006.243777, DOI 10.1109/DATE.2006.243777]

[7]

Helmstetter C., 2014, LEIBNIZ T EMB SYS, V1

[8]

Herber P., 2008, P 6 IEEE ACM IFIP IN, P131, DOI DOI 10.1145/1450135.1450166

[9]

IEEE Standards Association, 2011, IEEE Std. 1666-2011

[10]

Karlsson D, 2006, DES AUT TEST EUROPE, P1228

← 1 2 →