Executing Model Checking Counterexamples in Simulink

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057861" target="_blank" >RIV/00216224:14330/12:00057861 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Executing Model Checking Counterexamples in Simulink
Original language description
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 paperwe 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).
Czech name
—
Czech description
—

Project
<a href="/en/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Software Components in Embedded Systems: Development and Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering
ISBN
9780769547510
ISSN
—
e-ISSN
—
Number of pages
4
Pages from-to
245-248
Publisher name
IEEE Computer Society
Place of publication
Neuveden
Event location
Beijing, China
Event date
Jul 4, 2012
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)