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
相关论文
共 50 条
  • [31] A Model Checker for Operator Precedence Languages
    Chiari, Michele
    Mandrioli, Dino
    Pontiggia, Francesco
    Pradella, Matteo
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2023, 45 (03):
  • [32] MCMT: A Model Checker Modulo Theories
    Ghilardi, Silvio
    Ranise, Silvio
    AUTOMATED REASONING, 2010, 6173 : 22 - +
  • [33] Implementation of CTL model checker update
    Cacovean, Laura F.
    Popa, Emil M.
    Brumar, Cristina I.
    PROCEEDING OF THE 11TH WSEAS INTERNATIONAL CONFERENCE ON COMPUTERS: COMPUTER SCIENCE AND TECHNOLOGY, VOL 4, 2007, : 431 - +
  • [34] Algebraic algorithm of CTL model checker
    Cacovean, Florentina Laura
    Popa, Emil Marin
    Brumar, Cristina Ioana
    Brumar, Bogdan Alexandru
    WSEAS Transactions on Information Science and Applications, 2007, 4 (01): : 1 - 8
  • [35] HYTECH: A model checker for hybrid systems
    Henzinger, TA
    Ho, PH
    Toi, HW
    COMPUTER AIDED VERIFICATION, 1997, 1254 : 460 - 463
  • [36] αCheck: A mechanized metatheory model checker
    Cheney, James
    Momigliano, Alberto
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2017, 17 (03) : 311 - 352
  • [37] PRISM: Probabilistic symbolic model checker
    Kwiatkowska, M
    Norman, G
    Parker, D
    COMPUTER PERFORMANCE EVALUATION: MODELLING TECHNIQUES AND TOOLS, 2002, 2324 : 200 - 204
  • [38] HyTech: A model checker for hybrid systems
    Henzinger T.A.
    Ho P.-H.
    Wong-Toi H.
    International Journal on Software Tools for Technology Transfer, 1997, 1 (1-2) : 110 - 122
  • [39] Automatic verification of a model checker by reflection
    Wang, BY
    PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, 2006, 3819 : 45 - 59
  • [40] The Mec 5 model-checker
    Griffault, A
    Vincent, A
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 488 - 491
12345