Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Formal Methods for Industrial Critical Systems (FMICS 2012)
ISBN
9783642324680
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
78-92
Publisher name
Springer Berlin Heidelberg
Place of publication
Berlin
Event location
Paříž
Event date
Aug 27, 2012
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—