SynQ: An Embedded DSL for Synchronous System Design with Quantitative Types
Rui Chen, Ingo Sander

TL;DR
SynQ is an embedded domain-specific language that uses quantitative types to enable formal, traceable, and semantically coherent design, verification, and implementation of synchronous embedded systems.
Contribution
It introduces SynQ, a novel embedded DSL based on quantitative type theory, for systematic and formal design of synchronous systems with integrated verification and code generation.
Findings
Facilitates formal specification and verification of synchronous systems.
Supports modeling, simulation, and code generation within a coherent framework.
Demonstrated through a case study showing practical applicability.
Abstract
System design automation aims to manage the design of embedded systems with ever-increasing complexity. To the success of system design automation, there is still a lack of systematic and formal design process because an entire design process, from a system's specification to its implementation, has to deal with inherent concerns about the systems' different aspects and, consequently, inherent semantic gaps. These gaps make it hard for a design process to be traceable or transparent. Particularly, guaranteeing the correctness of produced implementations becomes the main challenge for a system design process. SynQ (Synchronous system design with Quantitative types) is an embedded domain specification language (EDSL) targeting the design of systems obeying the perfect synchrony hypothesis. SynQ is based on a component-based design framework and, by design, facilitates semantic coherency…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsEmbedded Systems Design Techniques · Formal Methods in Verification · Model-Driven Software Engineering Techniques
