BARNAT, Jiří, Luboš BRIM, Jan BERAN, Tomáš KRATOCHVÍLA and Italo Romani DE OLIVEIRA. Executing Model Checking Counterexamples in Simulink. In Tiziana Margaria, Zongyan Qiu, and Hongli Yang. IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering. Neuveden: IEEE Computer Society, 2012, p. 245-248. ISBN 978-0-7695-4751-0.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Executing Model Checking Counterexamples in Simulink
Authors BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Jan BERAN (203 Czech Republic), Tomáš KRATOCHVÍLA (203 Czech Republic) and Italo Romani DE OLIVEIRA (76 Brazil).
Edition Neuveden, IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering, p. 245-248, 4 pp. 2012.
Publisher IEEE Computer Society
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/00216224:14330/12:00057861
Organization unit Faculty of Informatics
ISBN 978-0-7695-4751-0
Keywords in English LTL Model Checking; Simulink; Embedded Systems; DiVinE
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 10/4/2013 11:38.
Abstract
Verification of embedded systems has become increasingly important in many industrial domains. Safety critical embedded systems, such as those developed in aerospace industry, are regularly subject to automated formal verification process. In this paper we extend our tool integration chain of parallel, explicit-state LTL model checker DIVINE and Matlab Simulink tool suit with an improved support of counterexample simulation. In particular, we show how to provide the verification engineer with a direct connection between the error discovered by the model checker and the simulation in Matlab Simulink. This work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST).
Abstract (in Czech)
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.
Links
GAP202/11/0312, research and development projectName: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
PrintDisplayed: 6/9/2024 14:20