D 2012

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

BARNAT, Jiří, Jan BERAN, Luboš BRIM, Tomáš KRATOCHVÍLA, Petr ROČKAI et. al.

Základní údaje

Originální název

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Jan BERAN (203 Česká republika), Luboš BRIM (203 Česká republika, domácí), Tomáš KRATOCHVÍLA (203 Česká republika) a Petr ROČKAI (703 Slovensko, domácí)

Vydání

Berlin, Formal Methods for Industrial Critical Systems (FMICS 2012), od s. 78--92, 15 s. 2012

Nakladatel

Springer Berlin Heidelberg

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Francie

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/12:00057863

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-32468-0

ISSN

DOI

Klíčová slova anglicky

LTL Model Checking; Simulink; Embedded Systems; DiVinE

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 23. 4. 2013 13:18, RNDr. Pavel Šmerk, Ph.D.

Anotace

ORIG CZ

V originále

Embedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DIVINE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink/Stateflow as the primary design language. The work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST).

Česky

Vestavné systémy jsou nedílnou součástí mnoha kontrolních systémů, včetně systémů používaných v letectví. Tato doména je specifická tím, že vyžaduje od systémů vysokou úroveň kvality a bezpečnosti a minimum chyb. Přesto, při vývoji takovýchto systémů se pouze zřídka používají moderní metody verifikace software. Uvedený výsledek spočívá v intergraci nástrojů pro návrh (nástroje HiLiTe a MATLAB Simulink) a verifikaci (nástroj DiVinE) vestavných szstémů. Integrace umožní snažší použití formálních metod verifikace při vývoji vestavných systémů, což přirozeně vede k větší spolehlivosti a integritě těchto systémů. Výsledek byl dosažen v rámci řešení evropského projektu iFEST agentury Artemis Joint Undertaking.

Návaznosti

GAP202/11/0312, projekt VaV
Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GD102/09/H042, projekt VaV
Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty