Formal Verification of AADL Specifications in the Topcased Environment

被引:0
|
作者
Berthomieu, Bernard [1 ,2 ]
Bodeveix, Jean-Paul [2 ,3 ]
Chaudet, Christelle [2 ,3 ]
Dal Zilio, Silvano [1 ,2 ]
Filali, Mamoun [2 ,3 ]
Vernadat, Francois [1 ,2 ]
机构
[1] CNRS, LAAS, 7 Ave Colonel Roche, F-31077 Toulouse, France
[2] Univ Toulouse, UPS,UTM, INSA,UT1, INP,ISAE, F-31062 Toulouse, France
[3] Univ Toulouse, CNRS, IRIT, F-31062 Toulouse, France
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We describe a formal verification toolchain for AADL, the SAE Architecture Analysis and Design Language, enriched with its behavioral annex. Our approach is based on tools that are integrated in the Topcased environment. We give a high-level view of the tools involved and illustrate the successive transformations that take place during the verification process.
引用
收藏
页码:207 / +
页数:3
相关论文
共 50 条
  • [1] Formal Verification of AADL Models Using UPPAAL
    Goncalves, Fernando Silvano
    Pereira, David
    Tovar, Eduardo
    Becker, Leandro Buss
    [J]. 2017 VII BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEMS ENGINEERING (SBESC), 2017, : 117 - 124
  • [2] An Architecture-Based Verification Technique for AADL Specifications
    Johnsen, Andreas
    Pettersson, Paul
    Lundqvist, Kristina
    [J]. SOFTWARE ARCHITECTURE, 2011, 6903 : 105 - 113
  • [3] AADL execution semantics transformation for formal verification
    Abdoul, Thomas
    Champeau, Joel
    Dhaussy, Philippe
    Pillain, Pierre-Yves
    Roger, Jean-Charles
    [J]. ICECCS 2008: THIRTEENTH IEEE INTERNATIONAL CONFERENCE ON THE ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2008, : 263 - 268
  • [4] Formal Verification of AADL Models by Event-B
    Hadad, Abeer Saeed Abdo
    Ma, Chunyan
    Ahmed, Adeeb Abdulwakeel Obadi
    [J]. IEEE ACCESS, 2020, 8 : 72814 - 72834
  • [5] Formal Verification of Behavioral AADL Models by Stateful Timed CSP
    Zhang, Feng
    Zhao, Yongwang
    Ma, Dianfu
    Niu, Wensheng
    [J]. IEEE ACCESS, 2017, 5 : 27421 - 27438
  • [6] Contributions to Improvement of the Formal Properties Verification Process in AADL Programs
    de Oliveira, Rafael Garlet
    Santos, Gabriel H. R.
    Farines, Jean-Marie
    Becker, Leandro Buss
    [J]. 2011 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEM ENGINEERING (SBESC), 2011, : 27 - 32
  • [7] Formal verification and validation of interactive systems specifications -: From informal specifications to formal validation
    Aït-Ameur, Y
    Breholée, B
    Girard, P
    Guittet, L
    Jambon, F
    [J]. HUMAN ERROR, SAFETY AND SYSTEMS DEVELOPMENT, 2004, 152 : 61 - 76
  • [8] Formal Verification of Security Specifications with Common Criteria
    Morimoto, Shoichi
    Shigematsu, Shinjiro
    Goto, Yuichi
    Cheng, Jingde
    [J]. APPLIED COMPUTING 2007, VOL 1 AND 2, 2007, : 1506 - +
  • [9] A simulation approach to verification and validation of formal specifications
    Liu, SY
    [J]. FIRST INTERNATIONAL SYMPOSIUM ON CYBER WORLDS, PROCEEDINGS, 2002, : 113 - 120
  • [10] Modular formal verification of specifications of concurrent systems
    Gradara, Sara
    Santone, Antonella
    Vaglini, Gigliola
    Villani, Maria Luisa
    [J]. SOFTWARE TESTING VERIFICATION & RELIABILITY, 2008, 18 (01): : 5 - 28