Executing Model Checking Counterexamples in Simulink (2012)výskyt výsledku
Identifikační kód | RIV/00216224:14330/12:00057861 |
---|---|
Název v anglickém jazyce | Executing Model Checking Counterexamples in Simulink |
Druh | D - Článek ve sborníku |
Jazyk | eng - angličtina |
Obor - skupina | I - Informatika |
Obor | IN - Informatika |
Rok uplatnění | 2012 |
Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
Počet výskytů výsledku | 1 |
Počet tvůrců celkem | 5 |
Počet domácích tvůrců | 2 |
Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792) Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) Jan Beran (státní příslušnost: CZ - Česká republika) Tomáš Kratochvíla (státní příslušnost: CZ - Česká republika) Italo Romani de Oliveira (státní příslušnost: BR - Brazilská federativní republika) |
Popis výsledku v anglickém jazyce | 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). |
Klíčová slova oddělená středníkem | LTL Model Checking; Simulink; Embedded Systems; DiVinE |
Stránka www, na které se nachází výsledek | - |
Údaje o výsledku v závislosti na druhu výsledku
Název sborníku | IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering |
---|---|
ISBN | 9780769547510 |
ISSN | - |
Počet stran výsledku | 4 |
Strana od-do | 245-248 |
Název nakladatele | IEEE Computer Society |
Místo vydání | Neuveden |
Místo konání akce | Beijing, China |
Datum konání akce | 04.07.2012 |
Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
Předkladatel | Masarykova univerzita / Fakulta informatiky |
---|---|
Dodavatel | GA0 - Grantová agentura České republiky (GA ČR) |
Rok sběru | 2013 |
Specifikace | RIV/00216224:14330/12:00057861!RIV13-GA0-14330___ |
Datum poslední aktualizace výsledku | 04.09.2013 |
Kontrolní číslo | 43536912 |
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
Projekt podporovaný GA ČR v programu GA | GAP202/11/0312 - Vývoj a verifikace softwarových komponent v zapouzdřených systémech (2011 - 2013) |
---|