Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1075277,
author = {Barnat, Jiří and Beran, Jan and Brim, Luboš and Kratochvíla, Tomáš and Ročkai, Petr},
address = {Berlin},
booktitle = {Formal Methods for Industrial Critical Systems (FMICS 2012)},
doi = {http://dx.doi.org/10.1007/978-3-642-32469-7_6},
editor = {Mariëlle Stoelinga, Ralf Pinger},
keywords = {LTL Model Checking; Simulink; Embedded Systems; DiVinE},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Berlin},
isbn = {978-3-642-32468-0},
pages = {78--92},
publisher = {Springer Berlin Heidelberg},
title = {Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs},
year = {2012}
}
TY - JOUR
ID - 1075277
AU - Barnat, Jiří - Beran, Jan - Brim, Luboš - Kratochvíla, Tomáš - Ročkai, Petr
PY - 2012
TI - Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs
PB - Springer Berlin Heidelberg
CY - Berlin
SN - 9783642324680
KW - LTL Model Checking
KW - Simulink
KW - Embedded Systems
KW - DiVinE
N2 - 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. The work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST).
ER -
BARNAT, Jiří, Jan BERAN, Luboš BRIM, Tomáš KRATOCHVÍLA and Petr ROČKAI. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In Mari\"elle Stoelinga, Ralf Pinger. \textit{Formal Methods for Industrial Critical Systems (FMICS 2012)}. Berlin: Springer Berlin Heidelberg, 2012, p.~78--92. ISBN~978-3-642-32468-0. Available from: https://dx.doi.org/10.1007/978-3-642-32469-7\_{}6.
|
