This website uses cookies to make the content more user-friendly and effective. By using this website, you agree to the use of cookies. You can find additonal information about the use of cookies and the possibility of objecting to the use of cookies here.

25 - 27 February 2020 // Nuremberg, Germany

Conferences and supporting programme

back to day overview
Session 6.4: Software Engineering III Software Quality I

Static Analysis of Finite State Machines with Zero False Alarms Vortragssprache Englisch

Safety-critical embedded software has to satisfy stringent quality requirements. Safety standards require evidence that no critical run-time errors occur. One important class of runtime errors is caused by undefined or unspecified behavior of the programming language, including buffer overflows or data races. They may cause erroneous or erratic behavior, induce system failures, and constitute security vulnerabilities. A sound static analyzer reports all such defects in the code, or proves their absence. Sound static analyzers are based on abstract interpretation, a formal method for static program analysis which supports formal soundness proofs: it can be proven that no error is missed (from the class of errors under analysis). A modern sound analyzer is composed of various abstract domains, each covering specific program properties of interest. A simple abstract domain is the interval domain which provides an interval containing all possible values of a variable for each program point. In this article we present a novel abstract domain developed in the static analyzer Astrée. Finite state machines and state variables are automatically detected, and by trace partitioning the different states and transitions can be disambiguated. 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.

--- Date: 27.02.2019 Time: 15:00 - 15:30 Location: Conference Counter NCC Ost



Dr. Daniel Kästner

AbsInt Angewandte Informatik GmbH


The selected entry has been placed in your favourites!

If you register you can save your favourites permanently and access all entries even when underway – via laptop or tablet.

You can register an account here to save your settings in the Exhibitors and Products Database and as well as in the Supporting Programme.The registration is not for the TicketShop and ExhibitorShop.

Register now

Your advantages at a glance:

  • Advantage Save your favourites permanently. Use the instant access – mobile too, anytime and anywhere – incl. memo function.
  • Advantage The optional newsletter gives you regular up-to-date information about new exhibitors and products – matched to your interests.
  • Advantage Call up your favourites mobile too! Simply log in and access them at anytime.