Automatic Model Building and Verification of Embedded Software with UPPAAL

Embedded systems are becoming ubiquitous and taking more and more important part in our daily life. Increasingly complex functionality leads to higher develop cost and lower software quality. Model checking has the potential of alleviating these problems. In this paper, we present an approach to construct model directly from the source code. An embedded system design language, Virgil, is selected as the target. Without losing any information, the UPPAAL model is generated based on the typed intermediate language. The timing information and stack behavior are estimated and after merging the hardware platform model, the whole system can be simulated on the model checker and some safety and aliveness properties of the program are verified.