Synthesizing SystemC Code from Delay Hybrid CSP

TL;DR

This paper introduces a novel method and tool for automatically synthesizing SystemC code from verified delay hybrid systems modeled by Delay HCSP, extending previous work on delay-free models to include delays.

Contribution

It presents the first approach to synthesize SystemC code from delay hybrid systems modeled by Delay HCSP, incorporating delay differential equations.

Findings

Developed a tool for automatic translation from dHCSP to SystemC.

Extended verification and synthesis methods to delay hybrid systems.

Demonstrated the feasibility of code generation from delay models.

Abstract

Delay is omnipresent in modern control systems, which can prompt oscillations and may cause deterioration of control performance, invalidate both stability and safety properties. This implies that safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling may be erratic, and further the incorrectness of the executable code generated from these models. However, automated methods for system verification and code generation that ought to address models of system dynamics reflecting delays have not been paid enough attention yet in the computer science community. In our previous work, on one hand, we investigated the verification of delay dynamical and hybrid systems; on the other hand, we also addressed how to synthesize SystemC code from a verified hybrid system modelled by Hybrid CSP (HCSP) without delay. In this paper, we give a first attempt to synthesize SystemC code from a verified delay hybrid system modelled by Delay HCSP (dHCSP), which is an extension of HCSP by replacing ordinary differential equations (ODEs) with delay differential equations (DDEs). We implement a tool to support the automatic translation from dHCSP to SystemC.