Modeling and verification of real-time embedded systems with urgency

Real-time embedded systems are often designed with different types of urgencies such as delayable or eager, that are modeled by several urgency variants of the timed automata model. However, most model checkers do not support such urgency semantics, except for the IF toolset that model checks timed automata with urgency against observers. This work proposes an Urgent Timed Automata (UTA) model with zone-based urgency semantics that gives the same model checking results as absolute urgency semantics of other existing urgency variants of the timed automata model, including timed automata with deadlines and timed automata with urgent transitions. A necessary and sufficient condition, called complete urgency, is formulated and proved for avoiding zone partitioning so that the system state graphs are simpler and model checking is faster. A novel zone capping method is proposed that is time-reactive, preserves complete urgency, satisfies all deadlines, and does not need zone partitioning. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.     

UML-based hardware/software co-design platform for dynamically partially reconfigurable network security systems

The dynamic partial reconfiguration technology of FPGA has made it possible to adapt system functionalities at run-time to changing environment conditions. However, this new dimension of dynamic hardware reconfigurability has rendered existing CAD tools and platforms incapable of efficiently exploring the design space. As a solution, we proposed a novel UML-based hardware/software co-design platform (UCoP) targeting at dynamically partially reconfigurable network security systems (DPRNSS). Computation-intensive network security functions, implemented as reconfigurable hardware functions, can be configured on-demand into a DPRNSS at run-time. Thus, UCoP not only supports dynamic adaptation to different environment conditions, but also increases hardware resource utilization. UCoP supports design space exploration for reconfigurable systems in three folds. Firstly, it provides reusable models of typical reconfigurable systems that can be customized according to user applications. Secondly, UCoP provides a partially reconfigurable hardware task template, using which users can focus on their hardware designs without going through the full partial reconfiguration flow. Thirdly, UCoP provides direct interactions between UML system models and real reconfigurable hardware modules, thus allowing accurate time measurements. Compared to the existing lower-bound and synthesis-based estimation methods, the accurate time measurements using UCoP at a high abstraction level can more efficiently reduce the system development efforts.     

Model-based platform-specific co-design methodology for dynamically partially reconfigurable systems with hardware virtualization and preemption

To facilitate the development of the dynamically partially reconfigurable system (DPRS), we propose a model-based platform-specific co-design (MPC) methodology for DPRS with hardware virtualization and preemption. For DPRS analysis and validation, a model-based verification and estimation framework is proposed to make model-driven architecture (MDA) more realistic and applicable to the DPRS design. Considering inherent characteristics of DPRS and real-time system requirements, a semi-automatic 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) can support the direct interaction between the UML models and the real hardware architecture. Compared to the existing estimation methods, UCoP can provide accurate and efficient platform-specific verification and estimation. We also propose a hierarchical design that consists of a hardware virtualization mechanism for dynamically linking the device nodes, kernel modules, and on-demand reconfigurable hardware functions and a hardware preemption mechanism for further increasing the utilization of hardware resources per unit time. Further, we realize a dynamically partially reconfigurable network security system (DPRNSS) to show the applicability and practicability of the MPC methodology. The DPRNSS cannot only dynamically adapt some of its hardware functions at run-time to meet different system requirements, but also determine which mechanism will be used. Our experiments also demonstrate that the hardware virtualization mechanism can save the overall system execution time up to 12.8% and the hardware preemption mechanism can reduce up to 41.3% of the time required by reconfiguration-based methods.