Formal Models of Microcontroller Systems
T. Noll, G. Herberich, B. Schlich, C. Weise
Embedded systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models. This, together with other effects, leads to the well-known state explosion problem, meaning that the models of those systems grow exponentially in size as the number of components increases. Careful handling of nondeterminism is therefore crucial for obtaining efficient 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 formal computation models and state-space reduction techniques to tackle this problem. A first approach was taken by defining a general automata-based model for microcontrollers, taking into account both the hardware, the software, and the environment of the system. This model was used to prove the correctness of a particular abstraction method, called delayed nondeterminism, which resolves nondeterministic behavior only if and when this is required by the application code. More concretely, a simulation relation between the concrete and the abstract state space was established, thus showing the soundness of delayed nondeterminism with respect to "path-universal" verification logics such as ACTL and LTL.
Current efforts concentrate on extending the model to cover further abstraction techniques, and on the implementation of a tool component which automatically produces a state-space generator from the given microcontroller model.
T. Noll, G. Herberich, B. Schlich, C. Weise
Embedded systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models. This, together with other effects, leads to the well-known state explosion problem, meaning that the models of those systems grow exponentially in size as the number of components increases. Careful handling of nondeterminism is therefore crucial for obtaining efficient 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 formal computation models and state-space reduction techniques to tackle this problem. A first approach was taken by defining a general automata-based model for microcontrollers, taking into account both the hardware, the software, and the environment of the system. This model was used to prove the correctness of a particular abstraction method, called delayed nondeterminism, which resolves nondeterministic behavior only if and when this is required by the application code. More concretely, a simulation relation between the concrete and the abstract state space was established, thus showing the soundness of delayed nondeterminism with respect to "path-universal" verification logics such as ACTL and LTL.
Current efforts concentrate on extending the model to cover further abstraction techniques, and on the implementation of a tool component which automatically produces a state-space generator from the given microcontroller model.
