Static Analysis of Software: The Abstract Interpretation
Language: English
Pages: 331
ISBN: 1848213204
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).
LabVIEW Graphical Programming Cookbook
Natural Computing: DNA, Quantum Bits, and the Future of Smart Machines
Connectivity); – P4: a switch is associated with – at most – two itineraries. 1.5.2. Dynamic verification Dynamic verification is based on the partial or total execution of the system. DEFINITION 1.12. – Dynamic analysis [ISO 85]: a dynamic analyzer is a software tool analyzing the behavior of a program by monitoring its execution. This tool enables us to record the paths covered, execution times, resources consumed, etc. 1.5.2.1. Analysis of execution There are several types of execution.
42-54. ACM Press, 2006. [LER 11] LEROY X., DOLIGEZ D., GARRIGUE J., RÉMY D., VOUILLON J., The Objective Caml system, www. caml.inria.fr/pub/docs/manual-ocaml/index.html. [MAR 04] MARTEL M., “Validation of assembler programs for dsps: a static analyzer”, PASTE ‘04: Proceedings of the 5th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 8-13, ACM Press, 2004. [MAU 05] MAUBORGNE L., RIVAL X., “Trace partitioning in abstract interpretation based static.
Verification, is a generic term that can be applied to any tool that derives the dynamic properties of a program but without executing it. Most static analysis or verification tools only verify the complexity of the software and look for constructions that can potentially be dangerous. As described in [BES 10], these tools can usually find errors in the code, but will miss errors that are strongly dependent on data flow (such as run-time errors or design errors). Due to the fact that they do not.
With automatic production of code by a code generator. In this approach, control algorithms are mainly modeled and simulated using block Polyspace 129 diagrams and state machines. The code is then automatically generated from these models and deployed onto embedded microprocessors in target machines. The code produced can nonetheless be a mixture of generated code and manual code. In critical systems, the state of the art regarding V&V techniques recommends using simulation and verification,.
The Office of Compliance and the device was subject to recall. 3.13.4. Other examples of the use of Polyspace® Polyspace® has been used by numerous companies in various industries. The first users were those for which quality and reliability were important criteria. Here are other examples are described more briefly. 3.13.4.1. Tackling sudden acceleration problems In 2010, drivers reported to Toyota that their vehicles were prone to sudden accelerations. A company called Exponent carried out an.