Learning Centre

Model checking timed safety instrumented systems

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Lahtinen, Jussi
dc.date.accessioned 2011-11-28T13:17:49Z
dc.date.available 2011-11-28T13:17:49Z
dc.date.issued 2008
dc.identifier.isbn 978-951-22-9445-9
dc.identifier.issn 1797-5042
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/874
dc.description.abstract Defects in safety-critical software systems can cause large economical and other losses. Often these systems are far too complex to be tested extensively. In this work a formal verification technique called model checking is utilized. In the technique, a mathematical model is created that captures the essential behaviour of the system. The specifications of the system are stated in some formal language, usually temporal logic. The behaviour of the model can then be checked exhaustively against a given specification. This report studies the Falcon arc protection system engineered by UTU Oy, which is controlled by a single programmable logic controller (PLC). Two separate models of the arc protection system are created. Both models consist of a network of timed automata. In the first model, the controller operates in discrete time steps at a specific rate. In the second model, the controller operates at varying frequency in continuous time. Five system specifications were formulated in timed computation tree logic (TCTL). Using the model checking tool Uppaal both models were verified against all five specifications. The processing times of the verification are measured and presented. The discrete-time model has to be abstracted a lot before it can be verified in a reasonable time. The continuous-time model, however, covered more behaviour than the system to be modelled, and could still be verified in a moderate time period. In that sense, the continuous-time model is better than the discrete-time model. The main contributions of this report are the model checking of a safety instrumented system controlled by a PLC, and the techniques used to describe various TCTL specifications in Uppaal. The conclusion of the work is that model checking of timed systems can be used in the verification of safety instrumented systems. en
dc.format.extent viii, 56
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Helsinki University of Technology en
dc.publisher Teknillinen korkeakoulu fi
dc.relation.ispartofseries TKK reports in information and computer science en
dc.relation.ispartofseries 3 en
dc.subject.other Computer science en
dc.subject.other Electrical engineering en
dc.title Model checking timed safety instrumented systems en
dc.type D4 Julkaistu kehittämis- tai tutkimusraportti taikka -selvitys fi
dc.contributor.school Faculty of Information and Natural Sciences en
dc.contributor.school 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 safety instrumented systems en
dc.subject.keyword model checking en
dc.subject.keyword real-time en
dc.subject.keyword Uppaal en
dc.identifier.urn urn:nbn:fi:tkk-011462
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