Abstract
A failure of safety-critical software may cause high costs or even endanger human beings. Contemporary safety standards require to identify potential functional and non-functional hazards and to demonstrate that the software does not violate the relevant safety goals. Typically for ensuring functional program properties model-based testing is used while non-functional properties like occurrence of runtime errors are addressed by abstract interpretation-based static analysis. Hence the verification process is split into two distinct parts – currently without any synergy between them being exploited. In this article we present an approach to couple model-based testing with static analysis based on a tool coupling between Astrée and BTC Embedded Tester ®. Astrée reports all potential runtime errors in C programs. This makes it possible to prove the absence of runtime errors, but typically users have to deal with false alarms, i.e. spurious notifications about potential runtime errors. Investigating alarms to find out whether they are true errors which have to be fixed, or whether they are false alarms can cause significant effort. The key idea of this work is to apply model-based testing to automatically find test cases for alarms reported by the static analyzer. When a test case reproducing the error has been found, it has been proven that it is a true error; when no error has been found with full test coverage, it has been proven to be a false alarm. This can significantly reduce the alarm analysis effort and reduces the level of expertise needed to perform the code-level software verification. We describe the underlying concept and report on experimental results and future work.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
AbsInt GmbH. aiT Worst-Case Execution Time Analyzer Website, http://www.AbsInt.com/ait
AbsInt GmbH. StackAnalyzer Website, http://www.AbsInt.com/sa .
AbsInt GmbH. Astrée Website, http://www.AbsInt.com/astree .
Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. In: AIAA Infotech@Aerospace 2010, number AIAA-2010-3385, pp. 1–38. American Institue of Aeronautics and Astronautics (April 2010)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), San Diego, California, USA, June 7-14, pp. 196–207. ACM Press (2003)
BTC Embedded Systems AG. BTC BTC EmbeddedTester ® Website, http://www.btc-es.de/index.php?idcatside=2 .
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
dSPACE GmbH. TargetLink Website, http://www.dSPACE.com/go/TargetLink
Esterel Technologies. SCADE Suite, http://www.esterel-technologies.com/products/scade-suite
Ferdinand, C., Heckmann, R.: Static Memory and Execution Time Analysis of Embedded Code. SAE 2006 Transactions Journal of Passenger Cars - Electronic and Electrical Systems 9 (2007)
ISO/IEC 9899:1999 (E). Programming languages – C (1999)
Kästner, D., Brockmeyer, U., Pister, M., Nenova, S., Bienmüller, T., Dereani, A., Ferdinand, C.: Combining Model-based Analysis and Testing. In: Embedded Real Time Software and Systems Congress ERTS2 (2014)
Kästner, D., Ferdinand, C.: Proving the Absence of Stack Overflows. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 203–214. Springer, Heidelberg (2014)
Kästner, D., Wilhelm, S., Nenova, S., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Astrée: Proving the Absence of Runtime Errors. In: Embedded Real Time Software and Systems Congress ERTS2 (2010)
Souyris, J., Pavec, E.L., Himbert, G., Jégu, V., Borios, G., Heckmann, R.: Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation. In: Proceedings of the 5th International Workshop on Worst-case Execution Time (WCET 2005), Mallorca, Spain, pp. 21–24 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Salvi, S., Kästner, D., Bienmüller, T., Ferdinand, C. (2014). True Error or False Alarm? Refining Astrée’s Abstract Interpretation Results by Embedded Tester’s Automatic Model-Based Testing. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science, vol 8696. Springer, Cham. https://doi.org/10.1007/978-3-319-10557-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-10557-4_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10556-7
Online ISBN: 978-3-319-10557-4
eBook Packages: Computer ScienceComputer Science (R0)