Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

• 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
• 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