×

Understanding the origin of alarms in Astrée. (English) Zbl 1141.68376

Hankin, Chris (ed.) et al., Static analysis. 12th international symposium, SAS 2005, London, UK, September 7–9, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28584-9/pbk). Lecture Notes in Computer Science 3672, 303-319 (2005).
Summary: Static analyzers like Astrée are incomplete, hence, may produce false alarms. We propose a framework for the investigation of the alarms produced by Astrée, so as to help classifying them as true errors or false alarms that are due to the approximation inherent in the static analysis. Our approach is based on the computation of an approximation of a set of traces specified by an initial and a (set of) final state(s). Moreover, we allow for finer analyses to focus on some execution patterns or on some possible inputs. The underlying algorithms were implemented inside Astrée and used successfully to track alarms in large, critical embedded applications.
For the entire collection see [Zbl 1087.68004].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

ASTREE; Consit; TVLA; CSSV
PDF BibTeX XML Cite
Full Text: DOI