Formal Verification of SystemC-based Cyber Components

Cyber-Physical Systems (CPS) integrate physical and cyber components, where the latter are responsible for the computation part. Due to their steadily increasing complexity, these cyber components have to be modeled at high level of abstraction when creating a new CPS. Therefore, the Electronic System Level (ESL) emerged and a widely accepted ESL design language is SystemC. The main driver for abstraction in SystemC is Transaction Level Modeling (TLM) which allows describing complex communication without all the details. Since the SystemC TLM models are used for early software development and as reference for hardware implementation their correct functional behavior is crucial. Admittedly, the best possible verification quality can be achieved with formal approaches. However, formal verification of TLM models is a hard task. Existing methods basically consider local properties or have extremely high run-time. In contrast, the proposed approach can efficiently verify true TLM properties, for instance the effect of a transaction can be formally checked which has not been possible before. Our approach transforms the SystemC model to C, embeds the TLM property in form of assertions into the C model and finally uses a novel induction to check the validity of the property. The induction method is essentially a lifting of inductive bounded model checking to C. In experiments we show the efficiency of the approach.