From UML/MARTE Specifications to ESL HW/SW Co-Design: Early Functional Verification and Timing Validation

From UML/MARTE Specifications to ESL HW/SW Co-Design: Early Functional Verification and Timing Validation

연구 분야: Verification

학회: ICPE '23 Companion: Companion of the 2023 ACM/SPEC International Conference on Performance Engineering

The continuous adoption of embedded systems in the most diverse application domains contributes to the increasing complexity of their development. Hardware/Software Co-Design methodologies are usually employed to tackle the challenges deriving from even more stringent functional and non-functional requirements. Using these methodologies, several validation and verification steps can be carried out early in the design process using a unified, technology-independent system model. This work investigates the possibility of integrating formal functional verification and timing validation in a Hardware/Software Co-Design flow at the system-level of abstraction. Specifically, we introduce Co-V&V, namely an additional step that consists of two phases: (i) a transformation from UML/MARTE to UPPAAL Timed Automata, and (ii) a preliminary functional verification and timing validation that exploits the UPPAAL verifier. We describe the Co-V&V step through a case study characterized by a component-based architecture and reactive behavior. The verification and validation conducted with UPPAAL indicate that our approach is particularly effective in discovering design flaws located in the communication protocol as well as those arising from the internal behavior of components.