Numerical Static Analysis Of Interrupt-driven Programs

Embedded software often involves intensive numerical computations and suffers from a number of run-time errors,e.g.,division by zero,arithmetic overflow and array out of bound.The technique of numerical static analysis is of practical importance for checking the correctness of embedded software.However,most of the existing approaches of numerical static analysis consider sequential programs,while interrupts are a commonly used facility that introduces concurrency in embedded systems.Interrupts are a commonly used technique to introduce concurrency in embedded software.Moreover,interrupt-driven programs(IDP)are commonly used in some safety critical applications,such as aerospace,automobile and medical equipment.Therefore,a numerical static analysis approach is highly desired for embedded software with interrupts.In this paper,we propose a static analysis approach specifically for interrupt-driven programs based on sequentialization techniques.Previous work mainly focus on sequential programs or general multi-thread programs.However,IDPs have their own features,e.g.,the asymmetric preemption between tasks and interrupts,the time constraints for interrupts and IDPs use special synchronization mechanisms and so on.On one hand,using the analysis technique which is for sequential programs may cause unsound analysis results.On the other hand,using the analysis technique which is for general multi-thread programs may cause imprecise analysis results.Thereby,there is a great need to design an analysis technique which is specially for IDPs.We focus on the numerical property of IDPs in this thesis.The goal of this thesis includes: exploring the sequentialization method for IDPs,designing specific abstract domains for the features of the sequentialized IDPs,design specific inter-procedural analysis technique for the sequentialized IDPs.Major contributions fo this thesis are listed as follows.1)We present a so-called data flow dependency sequentialization(DF_SEQ).DF_SEQ considers the asymmetric preemption between tasks and interrupts in IDPs and takes the data flow dependency into consideration to reduce the scale of the sequentialized programs.Moreover,we consider the effects of interrupt mask register(IMR)operations for the data flow dependency between tasks and interrupts during sequentialization.2)We design two specific abstract domains for the features of the sequentialized programs,boolean flag abstract domain and syntactic abstract domain.The features of the sequentialized programs may cause imprecision.So we design abstract domain to improve the precision.For some once-fired interrupts,we use boolean flags to distinguish whether those interrupts are triggered or not.For a code pattern which cause imprecision for non-relational abstract domain,we design a syntactic abstract domain combined with the non-relational abstract domain to improve the analysis precision.3)We present an optimization method for inter-procedural analysis to improve the scalability of the numerical analysis.There main contains lots of function calls for the interrupts service routine in an sequentialized IDP,which is not common in the ordinary sequential programs.To solve this problem,based on the tabular inter-procedural method,we utilize different inter-procedural analysis method for different kind of interrupts,e.g.,for complex interrupts we use the tabular method to analyze,while for simple interrupts we use a pre-partition tabular method to analyze.The analysis method in this thesis provides different trade-offs between precision and efficiency and can be used in different kinds of IDPs.They have been implemented our numerical static analysis prototype tool,and the prototype tool finds many bugs in some industry applications.