Motivation High-performance real-time embedded applications, such us HDTV, video streaming and packet routing, motivate the use of multicore and multiprocessor hardware platforms offering multiple processing units. Besides, such applications are subject to mass customization, as many variations of the same product are delivered to the market with different price, performance, and functionality. However, in current industrial practices, application requirements and design constraints are spread out and do not easily integrate and propagate through the development process. Moreover, the increasing complexity of applications tends to enlarge the abstraction gap between application description and hardware. Therefore, the complexity of both software and hardware, together with the stringent performance requirements (e.g., timing, memory, ...), makes design, deployment, and customization extremely difficult, leading to costly development cycles which result in products with sub-optimal performance.

Objectives To overcome the aforementioned problems, the goal of the IMPLEM team is to develop code-generation tools based on formal languages and models must play the central role of mapping platform independent software into target execution platforms (operating system and hardware), while ensuring at compile time that non-functional requirements provided by system’s engineers will be met at runtime. Integrating in a software product line, formal analysis and synthesis techniques for handling non-functional constraints and heterogeneous architectures, is an innovative way to provide correct by construction code. This enables code generation for specific platforms (including software-to-processor mapping and scheduling), and platform-independent functional analysis, to be linked together in the same tool-chain without semantic gap.

Outcome Such frameworks will considerably increase the overall quality of industrial systems designed with these tools, guaranteeing the correctness of the resulting solution. This approach enhances the applicability of formal verification and analysis techniques in industrial design flows, leading to a significant reduction in overall system’s validation time.