A Model Checker for AADL

被引:0
作者
Bozzano, Marco [1 ,2 ]
Cimatti, Alessandro [1 ,2 ]
Katoen, Joost-Pieter
Nguyen, Viet Yen
Noll, Thomas
Roveri, Marco [1 ,2 ]
Wimmer, Ralf [3 ]
机构
[1] Fdn Bruno Kessler, Trento, Italy
[2] Fdn Bruno Kessler, Trento, Italy
[3] Univ Freiburg, Freiburg, Germany
来源
COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2010年 / 6174卷
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying safety-critical systems by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA tables and dynamic fault trees, to performability evaluation, and diagnosability analysis. The toolset is currently being applied to several case studies by a major industrial developer of aerospace systems.
引用
收藏
页码:562 / +
页数:2
相关论文
共 11 条
  • [1] Model-checking algorithms for continuous-time Markov chains
    Baier, C
    Haverkort, B
    Hermanns, H
    Katoen, JP
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) : 524 - 541
  • [2] The FSAP/NuSMV-SA safety analysis platform
    Bozzano M.
    Villafiorita A.
    [J]. International Journal on Software Tools for Technology Transfer, 2007, 9 (01) : 5 - 24
  • [3] BOZZANO M, 2010, P ERTS 2010 IN PRESS
  • [4] BOZZANO M, 2009, P MEMOCODE 09, P121
  • [5] BOZZANO M, 2009, P ACES MB 09, P87
  • [6] BOZZANO M, 2010, COMPUTER J MAR, DOI DOI 10.1093/CO7
  • [7] Bozzano M, 2009, LECT NOTES COMPUT SC, V5775, P173, DOI 10.1007/978-3-642-04468-7_15
  • [8] CHKOURI MY, 2008, P ACES MB 08, P39
  • [9] Dwyer M. B., 1999, Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), P411, DOI 10.1109/ICSE.1999.841031
  • [10] Grunske L, 2008, ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, P31, DOI 10.1145/1368088.1368094