kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Quantitative Type Approach to Formal Component-Based System Design
KTH, School of Electrical Engineering and Computer Science (EECS), Electrical Engineering, Electronics and Embedded systems.
KTH, School of Electrical Engineering and Computer Science (EECS), Electrical Engineering, Electronics and Embedded systems.ORCID iD: 0000-0003-4859-3100
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

Available from: 2024-11-11 Created: 2024-11-11 Last updated: 2025-06-12Bibliographically approved

Open Access in DiVA

fulltext(489 kB)13 downloads
File information
File name FULLTEXT01.pdfFile size 489 kBChecksum SHA-512
66406e5eec82c1d95ed94ef844de293204ee73e81c1c14e3bbb76920be5258a7ae3c4fb6900a8a97a33058c3c7811801af337f9f1c8258c00986bf44867f2178
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records

Chen, RuiSander, Ingo

Search in DiVA

By author/editor
Chen, RuiSander, Ingo
By organisation
Electronics and Embedded systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 13 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 108 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf