Synthesizing SystemC Code from Delay Hybrid CSP

DOI10.1007/978-3-319-71237-6_2MaRDI QIDQ5055993zbMATH OpenOpenAlexFDO

Authors Gaogao Yan, Li Jiao, Naijun Zhan, Shu-Ling Wang

Publication date 9 December 2022

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1709.09019

zbMATH Keywords

SystemCcode generationapproximate bisimulationdelay dynamical systemsdelay hybrid CSP

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by ordinary differential equations (93C15) Delay control/observation systems (93C43)

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.

Recommendations

• Switching controller synthesis for time-delayed hybrid systems
• Automatic verification of stability and safety for delay differential equations
• scientific article; zbMATH DE number 2143087
• Hybrid Systems: Computation and Control
• Formal modelling, analysis and verification of hybrid systems

Cites work

• scientific article; zbMATH DE number 6111396 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 1444338 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• A Lyapunov approach to incremental stability properties
• Approximate bisimulation and discretization of hybrid CSP
• Approximation Metrics for Discrete and Continuous Systems
• Automatic verification of stability and safety for delay differential equations
• Bounded invariant verification for time-delayed nonlinear networked dynamical systems
• Formal Verification of Simulink/Stateflow Diagrams
• Generating Reliable Code from Hybrid-Systems Models
• Hybrid Systems: Computation and Control
• Statecharts: a visual formalism for complex systems
• Symbolic models for nonlinear time-delay systems using approximate bisimulations
• Symbolic models for time-varying time-delay systems via alternating approximate bisimulation
• Synthesizing SystemC Code from Delay Hybrid CSP
• Validated simulation-based verification of delayed differential dynamics

Cited in

(3)

• Hybrid Systems: Computation and Control
• Switching controller synthesis for time-delayed hybrid systems
• Synthesizing SystemC Code from Delay Hybrid CSP

Describes a project that uses

Uses Software

• Esterel
• Charon
• LUSTRE

This page was built for publication: Synthesizing SystemC Code from Delay Hybrid CSP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055993)