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 条
  • [1] Hazard Analysis for AADL Model
    Wei, Xiaomin
    Dong, Yunwei
    Yang, Mengmeng
    Hu, Ning
    Ye, Hong
    2014 IEEE 20TH INTERNATIONAL CONFERENCE ON EMBEDDED AND REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS (RTCSA), 2014,
  • [2] The SmlMC model checker
    Boeke, W
    DR DOBBS JOURNAL, 2003, 28 (03): : 48 - +
  • [3] The JKIND Model Checker
    Gacek, Andrew
    Backes, John
    Whalen, Mike
    Wagner, Lucas
    Ghassabani, Elaheh
    COMPUTER AIDED VERIFICATION, CAV 2018, PT II, 2018, 10982 : 20 - 27
  • [4] The model checker SPIN
    Holzmann, GJ
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1997, 23 (05) : 279 - 295
  • [5] The SPINJA Model Checker
    de Jonge, Marc
    Ruys, Theo C.
    MODEL CHECKING SOFTWARE, 2010, 6349 : 124 - 128
  • [6] Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL
    Bae, Kyungmin
    Olveczky, Peter Csaba
    FORMAL ASPECTS OF COMPONENT SOFTWARE, FACS 2023, 2024, 14485 : 127 - 152
  • [7] Using AADL to model a protocol stack
    Delanote, Didier
    Van Baelen, Stefan
    Joosen, Wouter
    Berbers, Yolande
    ICECCS 2008: THIRTEENTH IEEE INTERNATIONAL CONFERENCE ON THE ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2008, : 277 - 281
  • [8] The KIND 2 Model Checker
    Champion, Adrien
    Mebsout, Alain
    Sticksel, Christoph
    Tinelli, Cesare
    COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II, 2016, 9780 : 510 - 517
  • [9] MMC: the Mono Model Checker
    Ruys, Theo C.
    Aan de Brugh, Niels H. M.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 190 (01) : 149 - 160
  • [10] Model Checker Execution Reports
    Castano, Rodrigo
    Braberman, Victor
    Garbervetsky, Diego
    Uchitel, Sebastian
    PROCEEDINGS OF THE 2017 32ND IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE'17), 2017, : 200 - 205
12345