Executing Model Checking Counterexamples in Simulink

Logo poskytovatele

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ří 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

Citace
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:

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