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 条
  • [41] Towards a Spatial Model Checker on GPU
    Bussi, Laura
    Ciancia, Vincenzo
    Gadducci, Fabio
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 : 188 - 196
  • [42] The Investigation of TLC Model Checker Properties
    Shkarupylo, Vadym Viktorovych
    Tomicic, Igor
    Kasian, Kostiantyn Mykolaiovych
    JOURNAL OF INFORMATION AND ORGANIZATIONAL SCIENCES, 2016, 40 (01) : 145 - 152
  • [43] MERIT: An Interpolating Model-Checker
    Caniart, Nicolas
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 162 - 166
  • [44] NUSMV: A new symbolic model checker
    Cimatti A.
    Clarke E.
    Giunchiglia F.
    Roveri M.
    International Journal on Software Tools for Technology Transfer, 2000, 2 (4) : 410 - 425
  • [45] A symbolic model checker for tccp programs
    Alpuente, M
    Falaschi, M
    Villanueva, A
    RAPID INTEGRATION OF SOFTWARE ENGINEERING TECHNIQUES, 2005, 3475 : 45 - 56
  • [46] A model checker for verifying ConGolog programs
    Kalantari, L
    Ternovska, E
    EIGHTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-02)/FOURTEENTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-02), PROCEEDINGS, 2002, : 953 - 954
  • [47] Fault localization using a model checker
    Griesmayer, Andreas
    Staber, Stefan
    Bloem, Roderick
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2010, 20 (02): : 149 - 173
  • [48] HyTech: A model checker for hybrid systems
    EECS Department, University of California, Berkeley, CA 94720, United States
    不详
    不详
    Int. J. Softw. Tools Technol. Trans., 1-2 (110-122):
  • [49] Carmen: Software Component Model Checker
    Plsek, Ales
    Adamek, Jiri
    QUALITY OF SOFTWARE ARCHITECTURES, PROCEEDINGS, 2008, 5281 : 71 - +
  • [50] HYPERPROB: A Model Checker for Probabilistic Hyperproperties
    Dobe, Oyendrila
    Abraham, Erika
    Bartocci, Ezio
    Bonakdarpour, Borzoo
    FORMAL METHODS, FM 2021, 2021, 13047 : 657 - 666
12345