Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2012
Druh Článek ve sborníku
Konference Formal Methods for Industrial Critical Systems (FMICS 2012)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-32469-7_6
Obor Informatika
Klíčová slova LTL Model Checking; Simulink; Embedded Systems; DiVinE
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.