Model-Based Verification and Estimation Framework for Dynamically Partially Reconfigurable Systems

摘要

Unified Modeling Language (UML), an industry de-facto standard, has been used to analyze dynamically partially reconfigurable systems (DPRS) that can reconfigure their hardware functionalities on-demand at runtime. To make model-driven architecture (MDA) more realistic and applicable to the DPRS design in an industrial setting, a model-based verification and estimation (MOVE) framework is proposed in this work. By taking advantage of the inherent features of DPRS and considering real-time system requirements, a semiautomatic model translator converts the UML models of DPRS into timed automata models with transition urgency semantics for model checking. Furthermore, a UML-based hardware/software co-design platform (UCoP) is proposed to support the direct interaction between the UML models and the real hardware architecture. The two-phase verification process, including exhaustive functional verification and physical-aware performance estimation, is completely model-based, thus reducing system verification efforts. We used a dynamically partially reconfigurable network security system (DPRNSS) as a case study. The related experiments have demonstrated that the model checker in MOVE can alleviate the impact of the state-space-explosion problem. Compared to the synthesis-based estimation method having inaccuracies ranging from $-$43.4% to 18.4%, UCoP can provide accurate and efficient platform-specific verification and estimation through actual time measurements.