Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

Varování

Publikace nespadá pod Filozofickou 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:	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ů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace Software Components in Embedded Systems: Development and Verification