We present SynQ, an embedded DSL (EDSL) targeting synchronous system design with quantitative types. SynQ is designed to facilitate semantically coherent system design processes by language embedding and advanced type systems. The current case study indicates the potential for a seamless system design process.

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.

Model-driven engineering (MDE) addresses the complexity of modern-day embedded system design. Multiple MDE frameworks are often integrated into a design process to use each MDE framework's state-of-the-art tools for increased productivity. However, this integration requires substantial development effort. In this paper, we propose an MDE, framework based on a formalism of system graphs and trait hierarchies for programming-language-agnostic integration between tools within our framework and with tools of other MDE frameworks. Implementing our framework for each programming language is a one-time development effort. We evaluate our proposal in an MDE design process by developing a Java supporting library and an AMALTHEA connector. Then we perform an MDE, industrial avionics case study with both. The evaluation shows that our framework facilitates the integration of different tools and the independent development of different system parts. Therefore, our framework is a reliable MDE, framework that lowers the effort of integrating tools to benefit from their combined state-of-the-art.

New methodologies are needed for the development of avionics systems to meet today’s software explosion in complexity and related cost due to the increased functionality in the aircraft. Current design flows for software-intensive systems do not have a clear path from the functional specification to the final implementation and cannot provide real-time guarantees. The situation will become even more difficult because, in the future, more and more applications will share the same computation nodes and the network in a distributed hierarchical network-based system. In order to overcome the present situation, a novel methodology for a correct-by-construction design of safety-critical embedded avionics systems has been created and formulated within the Vinnova NFFP7 project CORRECT. Correct-by-construction design is a radical departure from current design practice, with the potential to decrease the verification costs for future systems significantly. The paper presents the underlying foundation of the methodology, its carefully selected ingredients, and discuss available results and existing tool support. The methodology is based on a disciplined system modelling environment grounded on a sound formal foundation, a design space exploration technique, and a clear path to hardware and software synthesis. An industrial case study investigates the potential of the methodology.