Research On Runtime Verification Method Of Embedded System Based On ARM Hardware-assisted Tracing

Embedded systems deeply connect the information world and the physical world,which puts forward higher requirements for the performance of embedded systems.Traditional analysis and evaluation(testing,simulation)cannot fully guarantee that the system reflects real requirements and behaviours,and cannot meet the requirements of reliability and safety,and more effective methods must be adopted to implement the analysis and verification of embedded systems.Runtime verification uses formal methods to describe system behaviour,and dynamically analyze the specific execution trajectory of the monitored system,to effectively analyze and verify the real system at runtime.The characteristics of hardwareassisted tracing are less invasive to solve the main contradiction of embedded system runtime verification-obtaining runtime information on resource-constrained embedded systems should have little or no overhead,this article aims to apply hardware-assisted tracing to embedded system runtime verification,the work content is mainly carried out from the following four aspects:(1)Design and implementation of runtime verification method for an embedded system based on ARM hardware-assisted tracing.For the embedded system of the ARM Cortex-M series,the framework HAT-RV,ITM and DWT components designed and implemented the embedded system runtime verification scheme based on hardware-assisted tracing are designed and implemented as kernel debugging hardware to obtain instruction-level operation information in operation with low intrusiveness,the PL(FPGA)side of the heterogeneous platform analyzes the tracing data online real-timeline and reconstructs the program trajectory,and the monitor implemented on the same platform receives the limited trajectory to verify whether the embedded system violates the properties.(2)The LTL3 properties are mapped to an alphabet that the underlying hardware monitor can receive through a three-layer abstraction mechanism.According to the characteristics of ITM components and DWT components and the semantic requirements of atomic proposition mapping,the runtime state abstraction is divided into three layers,and the linear sequential logic language LTL3 suitable for the runtime verification semantics of embedded systems is selected to describe the system attributes,in which the user interface layer uses four atomic propositional semantic types to declare key attributes,software layer hardware-assisted tracing configuration,hardware layer real-time tracing flow analysis,and step by layer between the three layers to abstract the system into a discrete system running in a series of discrete steps.(3)Implement a HAT-RV overlay that supports parallel,dynamic loading of reconfigurable monitors,and construct a HAT-RV property library for typical LTL property patterns.Consider that the monitor is an interactive and iterative process,using the PYNQ architecture,to implement the HAT-RV overlay,the overlay user through the Python interface to achieve PS and PL interaction,through the interaction to complete the PERI＿AP configuration,verification result query,atomic event stream storage;Based on the toolchain provided in this article to generate refactored monitors,construct dynamically loadable monitors;Complete overlay mapping and monitor loading in the web interface,mask the implementation details of the underlying hardware,and construct the HAT-RV property library for typical LTL attribute patterns to improve the efficiency and flexibility of runtime verification.(4)The effectiveness and flexibility of HAT-RV were verified through case analysis and performance evaluation.Through the application of the traffic light control system and the HATRV property library,the properties of the four atomic proposition types are verified,and the performance is evaluated from three aspects,the monitoring overhead HAT-RV static resource consumption is 0,and the increase in execution time caused by the tracing configuration is minimal,among which the increase in execution time of SOFT-RV is 6.9 times that of HAT-RV;in FPGA resource consumption,the overall resource utilization of static logic is not higher than15%.The usage rate of Slice resources with the highest dynamic logic usage does not exceed20%,so users do not need to worry about the proportion of resources after the implementation of complex monitors.In the time consumption,the average time spent per monitor is less than7 min,reducing the time consumed by the FPGA comprehensive implementation,whether it is a static bit stream or a partial bitstream loading,it will not exceed 0.6s.