Diagrams are helpful tools serving as visual representations of structured program data and models in model-driven engineering (MDE). However, existing solutions to create diagrams programmatically are often constrained to specific programming languages or limited in the support for pragmatic and interactive features known from diagramming frameworks. We here propose to provide diagrams as a service. The service is available through a web protocol. It provides a client that handles all diagram-related calculations for graph-based diagrams known from diagramming frameworks, including features such as automatic layout. JSON schemas for the diagram model and communication protocol facilitate automatic code generation and a direct connection to the service for custom diagram servers written in arbitrary programming languages. This enables interactive diagrams in any domain with established tooling. We evaluate the service, which is provided through the open-source KIELER framework, with two custom server implementations. The first example is a prototype written in Python that showcases different features of the service. The second example presents ForSyDe, a textual modeling environment developed in Haskell for formal system design. ForSyDe utilizes the diagram service to automatically generate dataflow visualizations of their code in VS Code.

The design process of safety-critical embedded systems is desired to be both practical and formal. These two requirements are consistently satisfied in a modern type-theory-based proof assistant/language that is increasingly accommodating general-purpose programming. A framework for embedded system design that satisfies both requirements can therefore be built upon such a proof assistant/language. In this paper, we present a framework for synchronous embedded system design that addresses both aspects (practicality and formality) by exploiting the quantitatively typed language Idris2. Specifically, we demonstrate that leveraging the expressiveness of quantitative type theory and the tagless final embedding enables an embedded domain-specific language (EDSL) named SynQ (Synchronous system design with Quantitative types) to be properly hosted in Idris2. This then allows Idris2 to be leveraged to facilitate synchronous system design (modelling, transformation, and implementation) and verification. It, hence, makes the presented framework a step towards an embedded system design methodology that is both practical and formal.

Raising the level of abstraction is considered key to addressing the ever-increasing complexity of embedded system design, but it causes additional challenges due to the larger abstraction gap between the initial specification and the final implementation. This article addresses the current lack of systematic design methods by extending existing design-transformation-based approaches and wrapping them into a rule-based transformational design methodology for heterogeneous multi-processor platforms. The methodology cross-fertilizes embedded system design with program transformation techniques while taking into account the interplay of tight constraints and platform heterogeneity inherent in such systems. It advocates step-wise transformations starting from initial requirements to yield a final refined model that is efficient for implementation.To consider the effect of transformations on different properties of the system at each step, the system is specified with a set of requirements, an application model, a platform model, and a set of mapping decisions; referred to as the RAMP view of the system. The RAMP view and its carefully selected underlying unified abstract graph representation lay the foundations for mechanizing and potentially automating design transformations. A pattern matching technique is introduced and a proof-of-concept tool is implemented that automatically detects all possible transformations by matching the patterns defined by the transformation rules to the abstract graph representation of the system model. The underlying graph representation enables complex transformations on different aspects of the design, resulting in an improved design space definition. The design space can be explored by application-platform co-exploration techniques, yielding the most promising sequence of application transformations alongside the best matching platform. The applicability and potential of the proposed methodology are showcased through the design of both an image processing system and a cloud detection system.

Due to strict timing requirements, designing embedded real-time systems for safety-critical applications is inherently complex. The design paradigm should not only be able to guarantee that the final system works but also fulfill the safety-critical specifications and requirements. This paper proposes a design approach for embedded systems using T-CREST, a time-predictable hardware platform, and ForSyDe, a modeling framework supporting the formal design of embedded systems. We designed different use cases, performed preliminary experiments, and demonstrated the possibility of using this method. Furthermore, we perform worst-case execution time (WCET) analysis of our example applications.

Modern type-theory-based proof assistants/languages are increasingly supporting general-purpose programming, making them both practical and formally rigorous. This dual nature aligns well with the needs of safety-critical embedded system design. It is hence promising that such a language can be employed as a proper meta-language for building an embedded system design framework that integrates reasoning and programming. In this paper, we demonstrate a unified framework for synchronous embedded system design, which leverages both aspects of the quantitatively typed language Idris2, with a focus on an embedded domain-specific language (EDSL), named SynQ, in the framework. Specifically, we show that the leveraging of the expressiveness of quantitative type theory and the tagless final embedding allows synchronous systems to be properly modelled by SynQ. This then enables a systematic usage of Idris2 for facilitating both design and verification of synchronous systems, demonstrating an initial step towards a correct-by-construction embedded system design process.

Concurrent process networks are a widely used parallel programming model for designing multiprocessor embedded systems, where system functionality is decomposed into processes that communicate via signals. These processes can be mapped onto different processing elements and executed concurrently. While the initial process network is designed to effectively capture high-level parallelism, it may not fully exploit the available parallelism. To enhance concurrency and balance workload distribution, process partitioning transformations are applied, restructuring process networks to expose finer-grained parallelism. The effectiveness of these transformations, however, depends on how well they align with the underlying hardware's parallel capabilities. A variety of partitioning transformations have been introduced for process networks constructed using higher-order functions in the form of process constructors and data-parallel skeletons. For such networks, algebraic laws of functions provide a principled foundation for defining transformation rules, enabling a systematic and non-ad-hoc approach to process network modification. However, selecting the most suitable transformation to optimize key performance metrics remains an open challenge. To address this, we propose a transformation strategy that systematically identifies the most effective partitioning transformations. Our approach introduces evaluation metrics and analytical models to assess the impact of parametric transformations across different configurations. We validate the proposed strategy through the transformation of two image processing algorithms, demonstrating that our analytical models correctly predict the most suitable transformations for enhancing parallelism and performance.

The increasing complexity of multiprocessor embedded systems demands automated design flows that bridge the gap between high-level specifications and efficient parallel implementations. Automatic parallelization via rule-based model transformations has proven promising, but navigating the vast transformation space remains challenging. We present an automated strategy that systematically guides transformation application, enabling performance-aware parallelization through scalable and targeted space exploration.Our approach employs attributed graphs as a formal and expressive intermediate representation for evaluating and applying model transformations. These graphs enrich nodes and edges with semantic properties (such as process types, execution costs, and communication dependencies), capturing both application structure and platform characteristics in a unified model.We evaluate our strategy on an image processing application using a prototype implementation. The tool autonomously reduces the number of transformations from 203 to 74 and shortens the exploration time from over 17 hours to under 12, while improving performance by filtering out non-beneficial transformations.

One of the main challenges of embedded system design lies in the natural heterogeneity of these systems. We can say that embedded systems are electronic systems designed and programmed to tackle a specific application. Each application has its requirements, although embedded systems often combine many domain-specific subsystems. Considering this context, the design of embedded systems can be extremely challenging, including system modeling, simulation, formal verification, and the synthesis to a correct implementation. To manage the complexity of such systems, the design should start at higher levels of abstraction, based on formal models, without considering the low-level characteristics of the underlying software or hardware. These high-level formal meta-models, named models of computation (MoC), define a set of rules that dictate how computation should be performed and how they should communicate with each other, along with other information such as the notion of time. In this paper, we present as the main contribution a set of rules and interfaces that enable the proper mixing of different MoC domains in a framework for complex embedded system design, thus allowing a heterogeneous system composition at a high abstraction level, including the synchronous reactive, synchronous dataflow, and scenario-aware dataflow MoCs. We model both part of an avionic system and a reconfigurable RISC-V processor using these MoCs and the proposed interfaces as a case study showing the applicability brought by our proposal.

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.

This article presents an elementary change detection algorithm designed using a synchronous model of computation (MoC) aiming at efficient implementations on parallel architectures. The change detection method is based on a 2D-first-order autoregressive ([2D-AR(1)]) recursion that predicts one-lag changes over bitemporal signals, followed by a high-parallelized spatial filtering for neighborhood training, and an estimated quantile function to detect anomalies. The proposed method uses a model-based on the functional language paradigm and a well-defined MoC, potentially enabling energy and runtime optimizations with deterministic data parallelism over multicore, GPU, or FPGA architectures. Experimental results over the bitemporal CARABAS-II SAR UWB dataset are evaluated using the synchronous MoC implementation, achieving gains in detection and hardware performance compared to a closed-form and well-known complexity model over the generalized likelihood ratio test (GLRT). In addition, since the one-lag AR(1) is a Markov process, its extension for a Markov chain in multitemporal (n-lags) analysis is applicable, potentially improving the detection performance still subject to high-parallelized structures.