A blended modeling framework for real-time design and verification of safety-critical embedded systems

Abstract

Embedded systems often require multiple representations for design, verification, and implementation, ranging from low-level programming languages to high-level formal models and domain-specific abstractions. Generally, synchronization among different representations or notations is achieved manually, a process that is labor-intensive and prone to mistakes, adversely impacting productivity and time-to-market objectives. Despite existing tool support, there remains a lack of unified, automated mechanisms that ensure semantic consistency across heterogeneous modeling and programming notations. This article presents a scalable blended modeling framework that automates the synchronizations across an extensible set of notations using bidirectional transformations. This facilitates the system development, comprising design and verification aspects of safety-critical embedded systems, using various notations interchangeably. The applicability of the proposed framework is demonstrated using four distinct representations: C, SystemVerilog, Timed Automata, and a domain-specific modeling language. The framework supports a notation-agnostic design flow, allowing development to begin from any of the supported languages. This enables seamless transitions across notations based on design or verification needs. Validated through two industrial case studies, a ventilator system and a cruise control system, the framework achieved high round-trip transformation accuracy with minimal information losses in edge cases such as language-specific keywords. Performance evaluations revealed low transformation latency and modest memory consumption, supported by efficient Abstract Syntax Tree (AST) traversal. This research lays the groundwork for the standardization of model-to-code, code-to-model, and code-to-code transformations, significantly reducing manual engineering effort and improving the reliability and agility of embedded systems design and verification processes.