Formal Methods in Development and Testing of Safety-Critical Applications

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F02%3A03074214" target="_blank" >RIV/68407700:21230/02:03074214 - 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 Applications

Popis výsledku v původním jazyce

The contribution addresses the application of formal methods in functional specification, design, verification and testing of real-time software systems in safety-critical applications. We present basic principles of software verification methods directed towards automatic proof of safety properties against the model of the system called model-checking. As an example, verification of a railway interlocking system developed by the AZD Prague Ltd. is proposed. Overview of testing methods for finite statemachines is also presented. We have developed a testing algorithm on the basis ofmodel-checking. We discuss advantages and drawbacks of the method and sketch topics for further research.

Název v anglickém jazyce

Formal Methods in Development and Testing of Safety-Critical Applications

Popis výsledku anglicky

The contribution addresses the application of formal methods in functional specification, design, verification and testing of real-time software systems in safety-critical applications. We present basic principles of software verification methods directed towards automatic proof of safety properties against the model of the system called model-checking. As an example, verification of a railway interlocking system developed by the AZD Prague Ltd. is proposed. Overview of testing methods for finite statemachines is also presented. We have developed a testing algorithm on the basis ofmodel-checking. We discuss advantages and drawbacks of the method and sketch topics for further research.

Druh

A - Audiovizuální tvorba

CEP obor

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

OECD FORD obor

—

Projekt

—

Návaznosti

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ů

ISBN

80-7149-452-1

Místo vydání

Pardubice

Název nakladatele resp. objednatele

Univerzita Pardubice

Verze

Neuveden

Identifikační číslo nosiče

—