Static Analysis of Software: The Abstract Interpretation
Format: PDF / Kindle (mobi) / ePub
The existing literature currently available to students and researchers is very general, covering only the formal techniques of static analysis.
This book presents real examples of the formal techniques called "abstract interpretation" currently being used in various industrial fields: railway, aeronautics, space, automotive, etc.
The purpose of this book is to present students and researchers, in a single book, with the wealth of experience of people who are intrinsically involved in the realization and evaluation of software-based safety critical systems. As the authors are people currently working within the industry, the usual problems of confidentiality, which can occur with other books, is not an issue and so makes it possible to supply new useful information (photos, architectural plans, real examples).
explosion: the number of states of the system is too great for analysis. There are then several solutions. We can: – implement optimization algorithms of the size of the graph in memory: for example BDDs (binary decision diagrams); 30 Static Analysis of Software – implement an abstraction of the model; – implement a strategy for the analysis of the system based on trajectories (partial analysis); – implement other state management strategies, for example we can replace the state memorization
has also become more complex as dynamic RAM with a one-page “cache” has been implanted on the CPU board. These new characteristics have the effect of making the execution time of an instruction from the program dependent on “what happened before”, and for a length of history that can be considerable. The method of calculating the WCET previously used for this type of control−command software has therefore become obsolete from the moment the processor has been retained. It has become too
pp. 627–633, Grenoble, France, 2009. [GOU 06] GOUBAULT E., PUTOT S., “Static analysis of numerical algorithms”, SAS’06, vol. 4134, pp. 18–34, Lecture Notes in Computer Science, Seoul, Korea, 2006. [GOU 08] GOUBAULT E., PUTOT S., “Perturbed affine arithmetic for invariant computation in numerical program analysis”, CoRR, abs/0807.2961, 2008. [HOA 69] HOARE C.A.R., “An axiomatic basis for computer programming”, ACM, vol. 12, no. 10, pp. 576-580, 1969. [IEE 85] IEEE, IEEE 754: Standard For
of the target application in a symbolic execution and verify dynamic properties. This symbolic execution requires the abstraction of concrete values into abstract values (lattice elements), and the computation of fixed points to cover the recursion often present in programs (loop, recursive function). These tools compute abstract values of each variable at each program point. The abstract value of a variable, v, represents all the values v can take during all possible executions of the program.
run-time errors. These errors must be instructed before being the other results can be used. Software Robustness 159 This is represented in Figure 4.9 by an arrow going from the run-time errors to the original code. Once the errors have been corrected, the static analysis tool produces the data dictionary and the call graph of the application. During the second stage, explained in section 4.5.2, static analysis is used to compute unknown functional domains and thus complete the definition of