Title: Applying formal methods to the configuration and verification of Trampoline RTOS
Authors: Jean-Luc Béchennec, Olivier H. Roux and Toussaint Tigori
Abstract: The low-level software of small embedded systems and especially the operating system must be configured and adapted to a given application. This specialization has several goals such as reducing memory usage, improving performance or removing dead code. However, traditional configuration methods do not guarantee that the component configured for the application continues to meet the specifications and it is not possible to use a test suite for the configured component since the test suite itself requires different configurations.
One possibility is to formally model the component at its source code level. Once completed by an application model, the parts of the component model that are not reachable correspond to dead code and can be removed. In this way a configured model is extracted. The verification of the component, whether it is configured or not, can be done by means of observers. Finally, since the modeling is done at the source code level, the configured component code can be generated.
