A. Chhokra, S. Abdelwahed, Abhishek Dubey, S. Neema, G. Karsai
2015 Electronic System Level Synthesis Conference (ESLsyn) 2015
SystemC designs lack formal semantics, making it difficult to perform automated verification and ensuring correctness of complex embedded systems. This work is innovative because it bridges the gap between practical SystemC development and formal methods by providing automatic code generation and verification through GME. This capability enables early detection of design errors and improves system reliability before hardware development.
This paper addresses the challenge of converting SystemC designs into formal verification models through a Generic Modeling Environment (GME)-based approach. The work develops an automated toolchain that translates SystemC specifications into intermediate representations and then to formal languages like Uppaal. The methodology supports both hardware and software aspects of cyber-physical systems, enabling designers to graphically model systems and automatically generate simulation code.
The approach successfully translates SystemC designs containing processes, ports, and state machines into Uppaal timed automata models. The tool generates deployable code from verified models and demonstrates the translation with a power system case study. Results show that the automated verification framework can identify behavioral issues and assist in design refinement.
@inproceedings{Chhokra2015,
author = {Chhokra}, A. and {Abdelwahed}, S. and Dubey, Abhishek and {Neema}, S. and {Karsai}, G.},
booktitle = {2015 Electronic System Level Synthesis Conference (ESLsyn)},
title = {From system modeling to formal verification},
year = {2015},
month = {jun},
pages = {41-46},
abstract = {Due to increasing design complexity, modern systems are modeled at a high level of abstraction. SystemC is widely accepted as a system level language for modeling complex embedded systems. Verification of these SystemC designs nullifies the chances of error propagation down to the hardware. Due to lack of formal semantics of SystemC, the verification of such designs is done mostly in an unsystematic manner. This paper provides a new modeling environment that enables the designer to simulate and formally verify the designs by generating SystemC code. The generated SystemC code is automatically translated to timed automata for formal analysis.},
category = {conference},
contribution = {minor},
file = {:Chhokra2015-From_system_modeling_to_formal_verification.pdf:PDF},
issn = {2117-4628},
keywords = {SystemC, formal verification, code generation, GME, model-based design, embedded systems, cyber-physical systems},
tag = {platform},
month_numeric = {6}
}