Automatically Generating SystemC Code from HCSP Formal Models

摘要

In model-driven design of embedded systems, how to generate code from high-level control models seamlessly and correctly is challenging. This is because hybrid systems are involved with continuous evolution, discrete jumps, and the complicated entanglement between them, while code only contains discrete actions. In this article, we investigate the code generation from Hybrid Communicating Sequential Processes (HCSP), a formal hybrid control model, to SystemC. We first introduce the notion of approximate bisimulation as a criterion to check the consistency between two different systems, especially between the original control model and the final generated code. We prove that it is decidable whether two HCSPs are approximately bisimilar in bounded time and unbounded time with some conditions, respectively. For both the cases, we present two sets of rules correspondingly for discretizing HCSPs and prove that the original HCSP model and the corresponding discretization are approximately bisimilar. Furthermore, based on the discretization, we define a transformation function to map a discretized HCSP model to SystemC code such that they are also approximately bisimilar. We finally implement a tool to automatically realize the translation from HCSP to SystemC code and illustrate our approach through some case studies.