Model checking embedded control software

Recently, embedded systems have become more and more complicated and thus traditional testing and simulation techniques for system validation are in many cases not sufficient. Additionally, the control of several real-world systems and processes require complex timing, which is difficult to verify with testing. The time scales of different delays can vary so much that the set of different timings possible to validate with testing is usually very limited. More powerful methods are needed and one formal method that can be used to verify and validate whether a complex system meets its requirements is model checking. The goal of this work is to evaluate the applicability of model checking for embedded control software. A general model checking methodology is given along with some central guidelines for modeling real-time control systems and, especially, the control software of those systems. Using the model checking methodology a part of the control firmware of an Uninterruptible Power Supply (UPS) is modeled with the model checking tool UPPAAL, which uses networks of timed automata as its modeling language. Ten failure cases related to the operation of the UPS were investigated and one or several specifications were formalized from each failure case using a temporal logic called Timed Computation Tree Logic (TCTL). The model of the system was verified against the system specifications and as a result of the verification two of the specifications were found to be violated. The results of the work indicate that model checking is a promising method for verifying and finding errors of timed software controlled embedded systems