Detailed Information on Publication Record
2012
Executing Model Checking Counterexamples in Simulink
BARNAT, Jiří, Luboš BRIM, Jan BERAN, Tomáš KRATOCHVÍLA, Italo Romani DE OLIVEIRA et. al.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
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
United States of America
Confidentiality degree
není předmětem státního či obchodního tajemství
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
Změněno: 10/4/2013 11:38, prof. RNDr. Luboš Brim, CSc.
V originále
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).
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 project |
|