Model checking embedded control software

No Thumbnail Available

URL

Journal Title

Journal ISSN

Volume Title

Faculty of Information and Natural Sciences |

Date

2010

Major/Subject

Mcode

Degree programme

Language

en

Pages

64

Series

TKK reports in information and computer science, 28

Abstract

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.

Description

Keywords

model checking, embedded software, real-time

Other note

Citation

Permanent link to this item

https://urn.fi/urn:nbn:fi:tkk-013112