Model checking embedded control software

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en Frits, Juho 2011-11-28T13:25:16Z 2011-11-28T13:25:16Z 2010
dc.identifier.isbn 978-952-60-3103-3
dc.identifier.issn 1797-5042
dc.description.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. en
dc.format.extent 64
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Aalto University School of Science and Technology en
dc.publisher Aalto-yliopiston teknillinen korkeakoulu fi
dc.relation.ispartofseries TKK reports in information and computer science en
dc.relation.ispartofseries 28 en
dc.subject.other Computer science en
dc.title Model checking embedded control software en Faculty of Information and Natural Sciences en Informaatio- ja luonnontieteiden tiedekunta fi
dc.contributor.department Department of Information and Computer Science en
dc.contributor.department Tietojenkäsittelytieteen laitos fi
dc.subject.keyword model checking en
dc.subject.keyword embedded software en
dc.subject.keyword real-time en
dc.identifier.urn urn:nbn:fi:tkk-013112
dc.type.dcmitype text en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication


My Account