A Quantitative Type Approach to Formal Component-Based System Design
2024 (English)In: 2024 forum on specification & design languages, FDL 2024, Institute of Electrical and Electronics Engineers (IEEE) , 2024, p. 27-36Conference paper, Published paper (Refereed)
Abstract [en]
Functional programming languages are recognised for their high abstraction level, high expressiveness, formal semantics, and correspondence to formal logic. However, the utilisation of functional languages in system design is limited because the existence of stateful, black-box components, e.g., simulation models and legacy components, breaks the functional languages' ground. Existing solutions to this situation, e.g. monads, are sub-optimal due to their ad-hoc and over-constrained nature. To address this challenge, we employ the quantitative type theory (QTT), which combines the dependent and linear (resource) type systems, for component specification. QTT enables stateful components to be used as pure functions with minimised restrictions. To this end, a functional language with QTT can be used for glue specification in a component-based design framework with all its advantages leveraged. The proposed approach is demonstrated by a case study in which a QTT-based RV32I instruction set architecture (ISA) specification in Idris2, a Haskell-like language, is simulated, verified, transformed and implemented in Verilog HDL by utilising properties of pure functions, which confirms the advantages of the proposed approach.
Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2024. p. 27-36
Series
International Forum on Design Languages, ISSN 1636-9874
Keywords [en]
embedded systems, component-based system design, functional language, quantitative type theory
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-356034DOI: 10.1109/FDL63219.2024.10673844ISI: 001324887800004Scopus ID: 2-s2.0-85206261708OAI: oai:DiVA.org:kth-356034DiVA, id: diva2:1912013
Conference
27th Forum on Specification and Design Languages (FDL), SEP 04-06, 2024, KTH Royal Inst Technol, Stockholm, SWEDEN
Funder
Vinnova, 2021-02484Vinnova, 2019-02743
Note
Part of ISBN 979-8-3315-0458-8, 979-8-3315-0457-1
QC 20241111
2024-11-112024-11-112025-06-12Bibliographically approved