Abstract
In safety-critical embedded software, the absence of critical code defects has to be demonstrated. One important class of defects are runtime errors caused by undefined or unspecified behavior of the programming language, including buffer overflows or data races. Sound static analyzers can report all such defects in the code (plus some possible false alarms), or prove their absence. A modern sound analyzer is composed of various abstract domains, each covering specific program properties of interest. In this article we present a novel abstract domain developed in the static analyzer Astrée. It automatically detects finite state machines and their state variables, and allows to disambiguate the different states and transitions by partitioning. Experimental results on real-life automotive and aerospace code show that embedded control software using finite state machines can be analyzed with close to zero false alarms, and that the improved precision can reduce analysis time.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Atiyah, M.F., Macdonald, I.G.: Introduction to Commutative Algebra. Addison-Wesley (1969)
Bodden, E.: Verifying finite-state properties of large-scale programs. Ph.D. thesis, McGill University (2009)
Bourdoncle, F.: Abstract interpretation by dynamic partitioning. J. Funct. Program. 2(4), 407–423 (1992)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977, pp. 238–252. ACM Press (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269–282. ACM Press, San Antonio (1979)
Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol. 17(2), 9:1–9:34 (2008)
Jeannet, B.: Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Formal Methods Syst. Des. 23(1), 5–37 (2003)
Kästner, D.: Applying abstract interpretation to demonstrate functional safety. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Industrial Complex Systems. ISTE/Wiley, London (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. 202–213. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10506-2_14
Kästner, D., Mauborgne, L., Ferdinand, C.: Detecting safety- and security-relevant programming defects by sound static analysis. In: Rainer Falk, J.-C.B., Chan, S. (eds.) The Second International Conference on Cyber-Technologies and Cyber-Systems (CYBER 2017). IARIA Conferences, vol. 2, pp. 26–31. IARIA XPS Press (2017)
Kästner, D., et al.: Finding all potential runtime errors and data races in automotive software. In: SAE World Congress 2017. SAE International (2017)
Kästner, D., Pohland, J.: Program analysis on evolving software. In: Roy, M. (ed.) CARS 2015 - Critical Automotive Applications: Robustness & Safety, France, Paris (2015)
Kästner, D., Schmidt, B., Schlund, M., Mauborgne, L., Wilhelm, S., Ferdinand, C.: Analyze this! sound static analysis for integration verification of large-scale automotive software. In: Proceedings of the SAE World Congress WCX2019 (SAE Technical Paper). SAE International (2019)
Mauborgne, L.: Astrée: verification of absence of runtime error. In: Jacquart, R. (ed.) Building the Information Society. IIFIP, vol. 156, pp. 385–392. Springer, Boston, MA (2004). https://doi.org/10.1007/978-1-4020-8157-6_30
Miné, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Logical Methods Comput. Sci. (LMCS) 8(26), 63 (2012)
Miné, A., Delmas, D.: Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software. In: Proceedings of the 15th International Conference on Embedded Software (EMSOFT 2015), pp. 65–74. IEEE CS Press, October 2015
Miné, A., et al.: Taking static analysis to the next level: proving the absence of run-time errors and data races with Astrée. Embedded Real Time Software and Systems Congress ERTS\(^2\) (2016)
Souyris, J., Le Pavec, E., 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) Analysis, pp. 21–24 (2005)
Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Software Eng. 12(1), 157–171 (1986)
Walkinshaw, N., Taylor, R., Derrick, J.: Inferring extended finite state machine models from software executions. Empirical Softw. Eng. 21(3), 811–853 (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Giet, J., Mauborgne, L., Kästner, D., Ferdinand, C. (2019). Towards Zero Alarms in Sound Static Analysis of Finite State Machines. In: Romanovsky, A., Troubitsyna, E., Bitsch, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2019. Lecture Notes in Computer Science(), vol 11698. Springer, Cham. https://doi.org/10.1007/978-3-030-26601-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-26601-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-26600-4
Online ISBN: 978-3-030-26601-1
eBook Packages: Computer ScienceComputer Science (R0)