Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057863" target="_blank" >RIV/00216224:14330/12:00057863 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-32469-7_6" target="_blank" >http://dx.doi.org/10.1007/978-3-642-32469-7_6</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-32469-7_6" target="_blank" >10.1007/978-3-642-32469-7_6</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

Popis výsledku v původním jazyce

Embedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DIVINE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink/Stateflow as the primary design language.

Název v anglickém jazyce

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

Popis výsledku anglicky

Embedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DIVINE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink/Stateflow as the primary design language.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2012

Kód důvěrnosti údajů

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

Název statě ve sborníku

Formal Methods for Industrial Critical Systems (FMICS 2012)

ISBN

9783642324680

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

78-92

Název nakladatele

Springer Berlin Heidelberg

Místo vydání

Berlin

Místo konání akce

Paříž

Datum konání akce

27. 8. 2012

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—