Astrée ("Analyseur statique de logiciels temps-réel embarqués") is a

static analyzer In computer science, static program analysis (or static analysis) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution. The term i ...

based on abstract interpretation. It analyzes programs written in

the C programming language ''The C Programming Language'' (sometimes termed ''K&R'', after its authors' initials) is a computer programming book written by Brian Kernighan and Dennis Ritchie, the latter of whom originally designed and implemented the language, as well as ...

and outputs an exhaustive list of possible runtime errors and

assertion Assertion or assert may refer to: Computing * Assertion (software development), a computer programming technique * assert.h, a header file in the standard library of the C programming language * Assertion definition language, a specification langu ...

violations. The defect classes covered include divisions by zero,

buffer overflows In information security and programming, a buffer overflow, or buffer overrun, is an anomaly whereby a program, while writing data to a buffer, overruns the buffer's boundary and overwrites adjacent memory locations. Buffers are areas of memor ...

, dereferences of

null Null may refer to: Science, technology, and mathematics Computing *Null (SQL) (or NULL), a special marker and keyword in SQL indicating that something has no value *Null character, the zero-valued ASCII character, also designated by , often used ...

dangling pointers Dangling pointers and wild pointers in computer programming are pointers that do not point to a valid object of the appropriate type. These are special cases of memory safety violations. More generally, dangling references and wild references ...

data race A race condition or race hazard is the condition of an electronics, software, or other system where the system's substantive behavior is dependent on the sequence or timing of other uncontrollable events. It becomes a bug when one or more of ...

deadlocks In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a loc ...

, etc. Astrée includes a static taint checker and helps finding cybersecurity vulnerabilities, such as

Spectre Spectre, specter or the spectre may refer to: Religion and spirituality * Vision (spirituality) * Apparitional experience * Ghost Arts and entertainment Film and television * ''Spectre'' (1977 film), a made-for-television film produced and writ ...

. The tool is tailored towards safety-critical embedded code: specific analysis techniques are used for common

control theory Control theory is a field of mathematics that deals with the control of dynamical systems in engineered processes and machines. The objective is to develop a model or algorithm governing the application of system inputs to drive the system to a ...

constructs (

finite state machines A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...

digital filters In signal processing, a digital filter is a system that performs mathematical operations on a sampled, discrete-time signal to reduce or enhance certain aspects of that signal. This is in contrast to the other major type of electronic filte ...

, rate limiters...) and

floating-point In computing, floating-point arithmetic (FP) is arithmetic that represents real numbers approximately, using an integer with a fixed precision, called the significand, scaled by an integer exponent of a fixed base. For example, 12.345 can be ...

numbers. Concurrent code is analyzed with a sound interleaving semantics that is aware of the concurrent threads of execution, their priorities and synchronization mechanisms. Astrée supports the

ARINC 653 ARINC 653 (Avionics Application Software Standard Interface) is a software specification for space and time partitioning in safety-critical avionics real-time operating systems (RTOS). It allows the hosting of multiple applications of different ...

OSEK OSEK (''Offene Systeme und deren Schnittstellen für die Elektronik in Kraftfahrzeugen''; English: "''Open Systems and their Interfaces for the Electronics in Motor Vehicles''") is a standards body that has produced specifications for an embedded o ...

and AUTOSAR execution models and can be adapted to additional OS specifications. On multi-core processors the placement of threads to cores, and the usage of mutex locks and

spinlock In software engineering, a spinlock is a lock that causes a thread trying to acquire it to simply wait in a loop ("spin") while repeatedly checking whether the lock is available. Since the thread remains active but is not performing a useful task, ...

s are taken into account. Astrée was developed in

Patrick Cousot Patrick Cousot (born 3 December 1948) is a French computer scientist, currently Silver Professor of Computer Science at the Courant Institute of Mathematical Sciences, New York University, USA. Before he was Professor at the École Normale Sup� ...

's group at

École Normale Supérieure École may refer to: * an elementary school in the French educational stages normally followed by secondary education Secondary education or post-primary education covers two phases on the International Standard Classification of Education sca ...

, a joint group with

CNRS The French National Centre for Scientific Research (french: link=no, Centre national de la recherche scientifique, CNRS) is the French state research organisation and is the largest fundamental science agency in Europe. In 2016, it employed 31,63 ...

, and is marketed by AbsInt GmbH. It is used in the defense/aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is

Airbus Airbus SE (; ; ; ) is a European multinational aerospace corporation. Airbus designs, manufactures and sells civil and military aerospace products worldwide and manufactures aircraft throughout the world. The company has three divisions: '' ...

. Astrée is a commercial product available from AbsInt Angewandte Informatik.

Bibliography

* Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival. ''Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software'', invited chapter. In ''The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones'', T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Volume 2566 of Lecture Notes in Computer Science, pp. 85–108, Springer. * Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival, ''A Static Analyzer for Large Safety-Critical Software.'', In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196–207, ACM. * David Delmas and Jean Souyris. ''Astrée: from Research to Industry.'', Proc. 14th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22–24 August 2007, LNCS 4634, pp. 437–451 * Arnaud J. Venet and Michael R. Lowry. 2010. Static analysis for software assurance: soundness, scalability and adaptiveness. In Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER '10). ACM, New York, NY, USA, 393-396. * Jean-Louis Boulanger. ''Static Analysis of Software: The Abstract Interpretation''. . Wiley. * Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. ''Astrée: Proving the Absence of Runtime Errors''. Embedded Real Time Software and Systems Congress ERTS², Toulouse, 2010. * A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, D. Kästner, S. Wilhelm, C. Ferdinand. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France. * D. Kästner, L. Mauborgne, N. Grafe, C. Ferdinand. Advanced Sound Static Analysis to Detect Safety- and Security-Relevant Programming Defects. 8th International Journal on Advances in Security, , vol. 11, no. 1 & 2, 149-159, IARIA, 2018. * D. Kästner, B. Schmidt, M. Schlundt, L. Mauborgne, S. Wilhelm, C. Ferdinand. Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software. SAE Technical Paper 2019-01-1246, SAE World Congress 2019, Detroit, April 2019.

References

External links

Astrée project academic page

Astrée industrial/sales page

{{DEFAULTSORT:Astree (static analysis) Abstract interpretation Static program analysis tools

See also

Bibliography

References

External links