SynQ: Synchronous System Design with Quantitative Types

QC 20261014

Abstract

Embedded systems increasingly underpin a safer, more efficient, and more connected modern life. Consequently, the number of embedded systems is growing, and so is the functionality they provide. This situation challenges the design and verification of embedded systems, especially the safety-critical ones, such as those in automotive, aerospace, and healthcare domains. It thus requires a system design process to be more automated and formally accountable/rigorous. The former allows the process to be more efficient and applicable to increasingly complex systems, while the latter allows the process to be more transparent and trustworthy for safety-critical systems. These two requirements for a design process are consistently satisfied in a modern, type-theory-based language/proof assistant that is increasingly accommodating general-purpose programming. Such a language allows computations and formal logic to be harmoniously combined in the type theory it implements. The computational aspect enables both executable models and applicable design steps to be defined in the language, which facilitates the design automation. Meanwhile, the logical aspect allows desired properties of the system and design steps to be formally specified and verified in the language, which promotes the accountability of a design process. Taken together, such a language and type theory can serve as an ideal meta-theory for such an aforementioned design process.

Motivated by the above, this monograph explores how Idris2, a quantitative type theory-based (QTT-based) language, can support formally accountable design processes for synchronous systems, a class of embedded systems commonly used in safety-critical signal-processing and control applications. Specifically, this monograph presents a component-based design framework, centred on the embedded domain-specific language SynQ (Synchronous System Design with Quantitative Types), in Idris2 for synchronous systems. By leveraging the tagless final embedding and the expressiveness of Idris2, especially its quantitative type system, the design framework: (1) allows stateful, black-box components to be safely used in a design process and be reasoned about in QTT; (2) allows systems to be modelled as function-like terms while being mapped to their implementations on different platforms by Idris2 functions; and (3) allows design transformations on system models to be defined as Idris2 functions. The first point guarantees that the design framework is compatible with common design practices. Meanwhile, the second and third points allow the entire design framework, including both system models and design steps (transformation and implementation-steps), to be defined in Idris2 and verified in QTT. With all these features, the design framework allows both the computational and logical aspects of Idris2 to be leveraged to deliver a formally accountable design process for synchronous systems. This monograph thus demonstrates how a modern type theory-based language can be leveraged for synchronous system design, and forms a step towards system design automation in general.

Link to DiVA