Research On Monitoring Technology For Embedded System Based On Runtime Verification

With the rapid development of information technology,embedded system as a flexible and dedicated operating system,has entered all aspects of people's lives.In some safety-critical areas,the failure of embedded systems can lead to extremely serious casualties and property damage.On the other hand,with the embedded operating system become more and more intelligent,networked and multi-media,the position of software in embedded system is also higher,and software more and more complex.How to implementate safety verification of the embedded system in the light of its characteristics,has received extensive attention and deep research in the academia and industry.Runtime verification is an emerging lightweight program verification technology,which monitors the operating state of the actual system to determine whether the implementation of the system meet the security needs.It is an effective complement of traditional software validation and validation technology.It can not only monitor the abnormal behavior of the system,but also run relevant code to repair system when security properties of the system are violated.Therefore,it is an effective idea to apply runtime verification technology to the behavior verification and system monitoring of embedded systems.Combined with the latest research results of runtime verification and the characteristics of embedded system,we mean to solve the problems encountered in the project in thesis.The main work is as follows:1.The expansion of specification language system.According to the problems encountered in the actual project,we extended the existing protocol language system,with Discrete-Time MTL applied to practical project research to catch the periodic properties and real-time properties in embedded system.2.Monitoring methods for periodic properties and real-time properties.Based on Discrete-Time MTL,we develop the monitoring framework of periodic properties and real-time properties.Two algorithms,from Discrete-Time MTL to automata,are designed and implemented.3.Monitoring methods for parametric temporal properties.Based on the trace slicing technique,the framework design for parameterized property monitoring is realized in the runtime verification framework for C programs,and the implementation is realized.4.Tools extension for embedded C program.Combined with LLVM compiler framework,we build the framework of runtime verification for embedded C programs,and the tool is implemented.