Synthesizing SystemC Code from Delay Hybrid CSP

DOI10.1007/978-3-319-71237-6_2zbMATH Open1503.68186arXiv1709.09019OpenAlexW2962792452MaRDI QIDQ5055993FDOQ5055993

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)

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.

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

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

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)

Cites Work

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

Cited In (3)

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

Uses Software

• LUSTRE
• Charon
• Esterel

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)