Formal Methods in Development and Testing of Safety-Critical Applications

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Formal Methods in Development and Testing of Safety-Critical Applications

Original language description

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.

Czech name

—

Czech description

—

Type

A - Audiovisual production

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2002

Confidentiality

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

ISBN

80-7149-452-1

Place of publication

Pardubice

Publisher/client name

Univerzita Pardubice

Version

Neuveden

Carrier ID

—