Compositional Verification for Component-Based Systems and Application

被引：0
|
作者：
Bensalem, Saddek [1 ]
Bozga, Marius [1 ]
Sifakis, Joseph [1 ]
Nguyen, Thanh-Hung [1 ]
机构：
[1] Univ Grenoble 1, CNRS, Verimag Lab, F-38041 Grenoble, France
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS | 2008年 / 5311卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transfer. The method is based oil the use of two kinds of invariants. Component invariants which are over-approximations of components' reachability sets. Interaction invariants which are constraints oil the states of components involved in interactions. Interaction invariants are obtained by computing traps of finite-state abstractions of the verified system. The method is applied for deadlock verification in the D-Finder tool. D-Finder is all interactive tool that takes as input BIP programs and applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants. The experimental results oil non-trivial examples allow either to prove deadlock-freedom or to identify very few deadlock configurations that call be analyzed by using state space exploration.
引用
收藏
页码：64 / 79
页数：16
相关论文
共 50 条
  • [1] Compositional verification for component-based systems and application
    Bensalem, S.
    Bozga, M.
    Nguyen, T. -H.
    Sifakis, J.
    [J]. IET SOFTWARE, 2010, 4 (03) : 181 - 193
  • [2] Runtime Verification of Component-Based Systems
    Falcone, Ylies
    Jaber, Mohamad
    Thanh-Hung Nguyen
    Bozga, Marius
    Bensalem, Saddek
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 204 - +
  • [3] Analysis of compositional conflicts in component-based systems
    Leicher, A
    Busse, S
    Süss, JG
    [J]. SOFTWARE COMPOSITION, 2005, 3628 : 67 - 82
  • [4] Compositional Abstraction Refinement for Component-Based Systems
    Zhang, Lianyi
    Meng, Qingdi
    Lo, Kueiming
    [J]. JOURNAL OF APPLIED MATHEMATICS, 2014,
  • [5] Verification of component-based software application families
    Xie, Fei
    Browne, James C.
    [J]. COMPONENT-BASED SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4063 : 50 - 66
  • [6] Verification of component-based systems with recursive architectures
    Bozga, Marius
    Iosif, Radu
    Sifakis, Joseph
    [J]. THEORETICAL COMPUTER SCIENCE, 2023, 940 : 146 - 175
  • [7] Incremental verification of component-based timed systems
    Julliand, J.
    Mountassir, H.
    Oudot, E.
    [J]. INTERNATIONAL JOURNAL OF COMPUTER APPLICATIONS IN TECHNOLOGY, 2011, 42 (2-3) : 159 - 176
  • [8] RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems
    Ben-Rayana, Souha
    Bozga, Marius
    Bensalem, Saddek
    Combaz, Jacques
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 : 394 - 406
  • [9] Refinement and verification of synchronized component-based systems
    Kouchnarenko, O
    Lanoix, A
    [J]. FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 341 - 358
  • [10] Specification and Verification of Component-based Systems (SAVCBS)
    Sharygina, Natasha
    [J]. IET SOFTWARE, 2008, 2 (06) : 475 - 476
12345