Formal Models of Microcontroller Systems
T. Noll, J. Brauer
Embedded systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models. Moreover they generally handle data spaces whose sizes grow with the memory and the word length of the respective microcontroller architectures. This, together with other effects, leads to the well-known state-space explosion problem, meaning that the models of those systems grow exponentially in size as the parameter values increase. Careful handling of both nondeterminism and large data spaces is therefore crucial for obtaining efficient methods and tools for analysis and verification.
The goal of this project, carried out in close cooperation with the Embedded Software Laboratory of our department, is to develop abstraction techniques to tackle this problem. With regard to control structures, a technique for refining loops in microcontroller programs has been developed. It is based on abstract interpretation using octagons and affine equalities in order to identify infeasible sequences of loop iterations. Our approach naturally integrates wraparound arithmetic during the generation of abstractions. Abstract interpreters operating on a refined control structure then typically derive strengthened program invariants without having to rely on complicated domain constructions.
With regard to data spaces, activities have been concentrating on static analysis methods for approximating the possible run-time values of data values. For this purpose, intervals have successfully been used for decades. Binary code on microcontroller platforms, however, is different from high-level code in that data is frequently altered using bit-wise operations and that the results of operations often depend on the hardware configuration. We therefore came up with a method that combines word- and bit-level interval analysis and that integrates a hardware model by means of abstract interpretation in order to handle these peculiarities. Both techniques have successfully been applied to a suite of benchmark examples.
T. Noll, J. Brauer
Embedded systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models. Moreover they generally handle data spaces whose sizes grow with the memory and the word length of the respective microcontroller architectures. This, together with other effects, leads to the well-known state-space explosion problem, meaning that the models of those systems grow exponentially in size as the parameter values increase. Careful handling of both nondeterminism and large data spaces is therefore crucial for obtaining efficient methods and tools for analysis and verification.
The goal of this project, carried out in close cooperation with the Embedded Software Laboratory of our department, is to develop abstraction techniques to tackle this problem. With regard to control structures, a technique for refining loops in microcontroller programs has been developed. It is based on abstract interpretation using octagons and affine equalities in order to identify infeasible sequences of loop iterations. Our approach naturally integrates wraparound arithmetic during the generation of abstractions. Abstract interpreters operating on a refined control structure then typically derive strengthened program invariants without having to rely on complicated domain constructions.
With regard to data spaces, activities have been concentrating on static analysis methods for approximating the possible run-time values of data values. For this purpose, intervals have successfully been used for decades. Binary code on microcontroller platforms, however, is different from high-level code in that data is frequently altered using bit-wise operations and that the results of operations often depend on the hardware configuration. We therefore came up with a method that combines word- and bit-level interval analysis and that integrates a hardware model by means of abstract interpretation in order to handle these peculiarities. Both techniques have successfully been applied to a suite of benchmark examples.