Static Analysis and Family-based Model Checking with VMC

被引：2

作者：

ter Beek, Maurice H. ^{[1
]}

Mazzanti, Franco ^{[1
]}

Damiani, Ferruccio ^{[2
]}

Paolini, Luca ^{[2
]}

Scarso, Giordano ^{[2
]}

Lienhardt, Michael ^{[3
]}

机构：

[1] ISTI CNR, Pisa, Italy

[2] Univ Turin, Turin, Italy

[3] Off Natl Etud & Rech Aerosp, Palaiseau, France

来源：

SPLC '21: PROCEEDINGS OF THE 25TH ACM INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE, VOL A | 2021年

关键词：

VMC; SPL; variability; FTS; MTS; static analysis; model checking;

D O I：

10.1145/3461001.3472732

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTS.). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTS. or a featured transition system (FTS).

引用

页数：1

共 50 条

[1] Static Analysis and Family-based Model Checking of Featured Transition Systems with VMC
ter Beek, Maurice H.
Mazzanti, Franco
Damiani, Ferruccio
Paolini, Luca
Scarso, Giordano
Valfre, Michele
Lienhardt, Michael
SPLC '21 - PROCEEDINGS OF THE 25TH ACM INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE, VOL B, 2021, : 24 - 27
[2] FTS4VMC: A front-end tool for static analysis and family-based model checking of FTSs with VMC
ter Beek, Maurice H.
Damiani, Ferruccio
Lienhardt, Michael
Mazzanti, Franco
Paolini, Luca
Scarso, Giordano
SCIENCE OF COMPUTER PROGRAMMING, 2022, 224
[3] Ariadne Hybridizing Directed Model Checking and Static Analysis
Milewicz, Reed
Pirkelbauer, Peter
2017 10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), 2017, : 442 - 447
[4] A Survey on Static Analysis and Model Checking
Garcia-Ferreira, Ivan
Laorden, Carlos
Santos, Igor
Garcia Bringas, Pablo
INTERNATIONAL JOINT CONFERENCE SOCO'14-CISIS'14-ICEUTE'14, 2014, 299 : 443 - 452
[5] Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL
Dimovski, Aleksandar S.
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2018), 2018, 10802 : 301 - 318
[6] Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
WenHui Zhang
Journal of Computer Science and Technology, 2003, 18 : 762 - 770
[7] Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
Zhang, WH
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2003, 18 (06) : 762 - 770
[8] Model checking of concurrent programs with static analysis of field accesses
Parizek, Pavel
Lhotak, Ondrej
SCIENCE OF COMPUTER PROGRAMMING, 2015, 98 : 735 - 763
[9] Model checking driven static analysis for the real world: designing and tuning large scale bug detection
Fehnker, Ansgar
Huuck, Ralf
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2013, 9 (01) : 45 - 56
[10] Model checking for malicious family detection and phylogenetic analysis in mobile environment
Cimino, Mario G. C. A.
De Francesco, Nicoletta
Mercaldo, Francesco
Santone, Antonella
Vaglini, Gigliola
COMPUTERS & SECURITY, 2020, 90

← 1 2 3 4 5 →