Formal Methods in Development and Testing of Safety-Critical Systems:Railway Interlocking System

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F02%3A03073474" target="_blank" >RIV/68407700:21230/02:03073474 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Formal Methods in Development and Testing of Safety-Critical Systems:Railway Interlocking System

Popis výsledku v původním jazyce

The contribution addresses the application of formal methods in functional specification, design and verification of real-time software systems in safety-critical applications. We present basic principles of software verification methods directed towardsautomatic proof of safety properties against the model of the system. Verification of the railway interlocking system developed by the AZD Prague Ltd. is presented. We discuss advantages and drawbacks of the presented methods and the possibility of us ing model-checking algorithms in the testing stage of the system development.

Název v anglickém jazyce

Formal Methods in Development and Testing of Safety-Critical Systems:Railway Interlocking System

Popis výsledku anglicky

The contribution addresses the application of formal methods in functional specification, design and verification of real-time software systems in safety-critical applications. We present basic principles of software verification methods directed towardsautomatic proof of safety properties against the model of the system. Verification of the railway interlocking system developed by the AZD Prague Ltd. is presented. We discuss advantages and drawbacks of the presented methods and the possibility of us ing model-checking algorithms in the testing stage of the system development.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/VS96047" target="_blank" >VS96047: Gerstnerova laboratoř pro inteligentní rozhodování a řízení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2002

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Intelligent Methods for Quality Improvement in Industrial Practice

ISBN

—

ISSN

—

e-ISSN

—

Počet stran výsledku

12

Strana od-do

14-25

Název nakladatele

ČVUT FEL, Katedra kybernetiky - Gerstnerova laboratoř

Místo vydání

Praha

Místo konání akce

Praha

Datum konání akce

11. 2. 2002

Typ akce podle státní příslušnosti

CST - Celostátní akce

Kód UT WoS článku

—