Towards Modular Verification of Software Product Lines with mCRL2

被引:0
|
作者
ter Beek, Maurice H. [1 ]
de Vink, Erik P. [2 ,3 ]
机构
[1] ISTI CNR, Pisa, Italy
[2] Eindhoven Univ Technol, Eindhoven, Netherlands
[3] CWI, Amsterdam, Netherlands
关键词
MODEL CHECKING; SYSTEMS; LOGICS;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We introduce by means of an example a modular verification technique for analyzing the behavior of software product lines using the mCRL2 toolset. Based on feature-driven borders, we divide a behavioral model of a product line into a set of separate components with interfaces and a driver process to coordinate them. Abstracting from irrelevant components, we verify properties over a smaller behavioral model, which not only simplifies the model checking task but also makes the result amenable for reuse. This is a fundamental step forward for the approach to scale up to industrial-size product lines.
引用
收藏
页码:368 / 385
页数:18
相关论文
共 50 条
  • [1] Modelling and Analysing Software in mCRL2
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    Luttik, Bas
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. FORMAL ASPECTS OF COMPONENT SOFTWARE, FACS 2019, 2020, 12018 : 25 - 48
  • [2] Tutorial: Designing Distributed Software in mCRL2
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 : 226 - 243
  • [3] An Overview of the mCRL2 Modelling and Verification Toolset
    Groote, Jan Friso
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (338): : 1 - 1
  • [4] Verification of networks of timed automata using mCRL2
    Groote, Jan Friso
    Reniers, Michel A.
    Usenko, Yaroslav S.
    [J]. 2008 IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL & DISTRIBUTED PROCESSING, VOLS 1-8, 2008, : 3782 - 3789
  • [5] Formal Modelling and Verification of an Interlocking Using mCRL2
    Bouwman, Mark
    Janssen, Bob
    Luttik, Bas
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2019, 2019, 11687 : 22 - 39
  • [6] Formal verification of OIL component specifications using mCRL2
    Olav Bunte
    Louis C. M. van Gool
    Tim A. C. Willemse
    [J]. International Journal on Software Tools for Technology Transfer, 2022, 24 : 441 - 472
  • [7] Formal Verification of OIL Component Specifications using mCRL2
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2020, 2020, 12327 : 231 - 251
  • [8] Formal verification of OIL component specifications using mCRL2
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (03) : 441 - 472
  • [9] Towards model checking executable UML specifications in mCRL2
    Hansen, Helle Hvid
    Ketema, Jeroen
    Luttik, Bas
    Mousavi, MohammadReza
    van de Pol, Jaco
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 83 - 90
  • [10] Formalising the Industrial Language SMMT in mCRL2
    van Laarhoven, Jordi E. P. M.
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2024, 2024, 14952 : 63 - 79