Executing Model Checking Counterexamples in Simulink

• Autoři: BARNAT Jiří; BRIM Luboš; BERAN Jan; KRATOCHVÍLA Tomáš; DE OLIVEIRA Italo Romani
• Rok publikování: 2012
• Druh: Článek ve sborníku
• Konference: IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: LTL Model Checking; Simulink; Embedded Systems; DiVinE
• Popis: Verifikace vestavných szstémů se stává stále důležitější součástí vývoje systémů v mnoha průmyslových odvětvích. Výsledkem této práce je integrace nástroje DiVinE, určeného pro formální verifikaci metodou ověřování modelu (LTL Model Checking) a nástroje MATLAB Simulink určeného mimojiné pro návrh vestavných systémů. Konkrétně se výsledek týka způsobu prezentace chyby odhalené v návrhu nástrojem DiVinE návrháři pracujícím s nástrojem Simulink. Výsledek vznikl v rámci řešení evropského projektu iFEST agentury Artemis Joint Undertaking.

Související projekty

• Software Components in Embedded Systems: Development and Verification