Executing Model Checking Counterexamples in Simulink

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:	Software Components in Embedded Systems: Development and Verification