Formal and Informal Methods for Multi-Core Design Space Exploration

TL;DR

This paper introduces a tool-supported methodology for exploring multi-core embedded system designs, enabling performance evaluation of various deployment strategies with uncertainty considerations, extending formal verification techniques.

Contribution

It presents a novel approach that combines formal verification with design-space exploration for multi-core embedded systems, including high-level modeling and uncertainty analysis.

Findings

Effective evaluation of deployment strategies

Enhanced formal verification scope

Support for uncertainty in performance assessment

Abstract

We propose a tool-supported methodology for design-space exploration for embedded systems. It provides means to define high-level models of applications and multi-processor architectures and evaluate the performance of different deployment (mapping, scheduling) strategies while taking uncertainty into account. We argue that this extension of the scope of formal verification is important for the viability of the domain.