More Web Proxy on the site http://driver.im/

research-article

VMC: recent advances and challenges ahead

Authors:

Maurice H. ter Beek,

Franco MazzantiAuthors Info & Claims

SPLC '14: Proceedings of the 18th International Software Product Line Conference: Companion Volume for Workshops, Demonstrations and Tools - Volume 2

Pages 70 - 77

https://doi.org/10.1145/2647908.2655969

Published: 15 September 2014 Publication History

Abstract

The variability model checker VMC accepts a product family specified as a Modal Transition System (MTS) with additional variability constraints. Consequently, it offers behavioral variability analyses over both the family and its valid product behavior. This ranges from product derivation and simulation to efficient on-the-fly model checking of logical properties expressed in a variability-aware version of action-based CTL. In this paper, we first explain the reasons and assumptions underlying the choice for a modeling and analysis framework based on MTSs. Subsequently, we present recent advances on proving inheritance of behavioral analysis properties from a product family to its valid products. Finally, we illustrate challenges remaining for the future.

References

[1]

A. Antonik, M. Huth, K. G. Larsen, U. Nyman, and A. Wąsowski. 20 Years of Modal and Mixed Specifications. Bulletin EATCS, 95:94--129, 2008.

[2]

P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. A Logical Framework to Deal with Variability. In Proceedings 8th International Conference on Integrated Formal Methods (IFM'10), volume 6396 of LNCS, pages 43--58. Springer, 2010.

Digital Library

[3]

P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. A Model-Checking Tool for Families of Services. In Proceedings 13th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'11), volume 6722 of LNCS, pages 44--58. Springer, 2011.

Digital Library

[4]

P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. Formal Description of Variability in Product Families. In Proceedings 15th International Software Product Lines Conference (SPLC'11), pages 130--139. IEEE, 2011.

Digital Library

[5]

M. H. ter Beek and E. P. de Vink. Using mCRL2 for the analysis of software product lines. In Proceedings 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE'14), pages 31--37. IEEE, 2014.

Digital Library

[6]

M. H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti. A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program., 76(2):119--135, 2011.

Digital Library

[7]

M. H. ter Beek, S. Gnesi, and F. Mazzanti. Demonstration of a model checker for the analysis of product variability. In Proceedings 16th International Software Product Line Conference (SPLC'12), volume 2, pages 242--245. ACM, 2012.

Digital Library

[8]

M. H. ter Beek, S. Gnesi, and F. Mazzanti. Model Checking Value-Passing Modal Specifications. In Perspectives of Systems Informatics, LNCS. Springer, 2014. To appear.

[9]

M. H. ter Beek, A. Lluch-Lafuente, and M. Petrocchi. Combining declarative and procedural views in the specification and analysis of product families. In Proceedings 17th International Software Product Line Conference (SPLC'13), volume 2, pages 10--17. ACM, 2013.

Digital Library

[10]

M. H. ter Beek, F. Mazzanti, and A. Sulova. VMC: A Tool for Product Variability Analysis. In Proceedings 18th International Symposium on Formal Methods (FM'12), volume 7436 of LNCS, pages 450--454. Springer, 2012.

[11]

E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM TOPLAS, 8(2):244--263, 1986.

Digital Library

[12]

A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Model checking software product lines with SNIP. STTT, 14(5):589--612, 2012.

Digital Library

[13]

A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program., 80:416--439, 2014.

Digital Library

[14]

A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE TSE, 39(8):1069--1089, 2013.

Digital Library

[15]

A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In Proceedings 32nd International Conference on Software Engineering (ICSE), volume 1, pages 335--344. ACM, 2010.

Digital Library

[16]

M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. ProVeLines: a product line of verifiers for software product lines. In Proceedings 17th International Software Product Line Conference (SPLC'13), volume 2, pages 141--146. ACM, 2013.

Digital Library

[17]

R. De Nicola and F. W. Vaandrager. Action versus State based Logics for Transition Systems. In Semantics of Systems of Concurrent Processes, volume 469 of LNCS, pages 407--419. Springer, 1990.

[18]

R. De Nicola and F. W. Vaandrager. Three logics for branching bisimulation. J. ACM, 42(2):458--487, 1995.

Digital Library

[19]

N. D'Ippolito, D. Fischbein, M. Chechik, and S. Uchitel. MTSA: The Modal Transition System Analyser. In Proceedings 23rd International Conference on Automated Software Engineering (ASE'08), pages 475--476. IEEE, 2008.

Digital Library

[20]

A. Fantechi and S. Gnesi. A behavioural model for product families. In Proceedings 6th Joint European Software Engineering Conference and International Symposium on Foundations of Software Engineering (ESEC/FSE'07), pages 521--524. ACM, 2007.

Digital Library

[21]

A. Fantechi and S. Gnesi. Formal modeling for product families engineering. In Proceedings 12th International Conference on Software Product Line Engineering (SPLC'12), pages 193--202. IEEE, 2008.

Digital Library

[22]

A. Fantechi, S. Gnesi, A. Lapadula, F. Mazzanti, R. Pugliese, and F. Tiezzi. A logical verification methodology for service-oriented computing. ACM TOSEM, 21(3):16, 2012.

Digital Library

[23]

D. Fischbein, S. Uchitel, and V. A. Braberman. A foundation for behavioural conformance in software product line architectures. In Proceedings Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA'06), pages 39--48. ACM, 2006.

Digital Library

[24]

S. Gnesi and F. Mazzanti. On the Fly Verification of Networks of Automata. In Proceedings International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), pages 1040--1046. CSREA Press, 1999.

[25]

S. Gnesi and F. Mazzanti. An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems. In Rigorous Software Engineering for Service-Oriented Systems, volume 6582 of LNCS, pages 390--407. Springer, 2011.

Digital Library

[26]

S. Gnesi and M. Petrocchi. Towards an executable algebra for product lines. In Proceedings 16th International Software Product Line Conference (SPLC'12), volume 2, pages 66--73. ACM, 2012.

Digital Library

[27]

A. Lapadula, R. Pugliese, and F. Tiezzi. A Calculus for Orchestration of Web Services. In Proceedings 16th European Symposium on Programming (ESOP'07), volume 4421 of LNCS, pages 33--47. Springer, 2007.

Digital Library

[28]

K. G. Larsen. Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion. Theoret. Comput. Sci., 72(2--3):265--288, 1990.

Digital Library

[29]

K. G. Larsen, U. Nyman, and A. Wąsowski. Modal I/O Automata for Interface and Product Line Theories. In Proceedings 16th European Symposium on Programming (ESOP'07), volume 4421 of LNCS, pages 64--79. Springer, 2007.

Digital Library

[30]

K. G. Larsen and B. Thomsen. A Modal Process Logic. In Proceedings 3rd Symposium on Logic in Computer Science (LICS'88), pages 203--210. IEEE, 1988.

[31]

K. Lauenroth, K. Pohl, and S. Töhning. Model Checking of Domain Artifacts in Product Line Engineering. In Proceedings 24th International Conference on Automated Software Engineering (ASE'09), pages 269--280, 2009.

Digital Library

[32]

M. Leucker and D. Thoma. A Formal Approach to Software Product Families. In Proceedings 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'12), volume 7609 of LNCS, pages 131--145. Springer, 2012.

Digital Library

[33]

R. Meolic, T. Kapus, and Z. Brezocnik. ACTLW: An action-based computation tree logic with unless operator. Inform. Sciences, 178(6):1542--1557, 2008.

Digital Library

[34]

J.-V. Millo, S. Ramesh, S. N. Krishna, and G. K. Narwane. Compositional Verification of Software Product Lines. In Proceedings 10th International Conference on Integrated Formal Methods (IFM'13), volume 7940 of LNCS, pages 109--123. Springer, 2013.

[35]

T. Thüm, S. Apel, C. Kästner, I. Schaefer, and G. Saake. A Classification and Survey of Analysis Strategies for Software Product Lines. Comput. Surv., 47(1):6:1--6:45, 2014.

Digital Library

Cited By

Casaluce RBurattin AChiaromonte FLafuente AVandin A(2024)White-box validation of quantitative product lines by statistical model checking and process miningJournal of Systems and Software10.1016/j.jss.2024.111983210:COnline publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.111983
Kishi T(2023)Family-based Model Checking using Probabilistic Model Checker PRISM2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00048(376-385)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00048
ter Beek MDamiani FLienhardt MMazzanti FPaolini LScarso G(2022)FTS4VMCScience of Computer Programming10.1016/j.scico.2022.102879224:COnline publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102879
Show More Cited By

Index Terms

VMC: recent advances and challenges ahead
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Software product line analysis with mCRL2
SPLC '14: Proceedings of the 18th International Software Product Line Conference: Companion Volume for Workshops, Demonstrations and Tools - Volume 2

The mCRL2 language and supporting software provide a state-of-the-art tool suite for the verification of distributed systems. In this paper, we present the general principles, extrapolated from [7,8], which make us believe that mCRL2 can also be used ...
Product Line Variability Modeling Based on Model Difference and Merge
COMPSACW '12: Proceedings of the 2012 IEEE 36th Annual Computer Software and Applications Conference Workshops

It is well known that the variability model, which captures the commonality and variability of the software product families, is very important to the software product line. Current software product line variability modeling methods relies on the ...
A modular product multi-platform configuration model

The product platform strategy has emerged as one of the important enablers of mass customisation where common components used across different product variants are maximised to decrease design, manufacturing and assembly cost. The Modular Product Multi-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SPLC '14: Proceedings of the 18th International Software Product Line Conference: Companion Volume for Workshops, Demonstrations and Tools - Volume 2

September 2014

151 pages

ISBN:9781450327398

DOI:10.1145/2647908

Editors:
Stefania Gnesi
ISTI-CNR, Italy
,
Alessandro Fantechi
University of Florence, Italy
,
Maurice H. ter Beek
ISTI-CNR, Italy
,
Goetz Botterweck
Lero, Ireland
,
Martin Becker
Fraunhofer IESE, Germany
,
General Chairs:
Stefania Gnesi
ISTI-CNR, Italy
,
Alessandro Fantechi
University of Florence, Italy

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

University of Florence: University of Florence
CNR: Istituto di Scienza e Tecnologie dell Informazione

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 September 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLC '14

Sponsor:

University of Florence
CNR

SPLC '14: 18th International Software Product Lines Conference - Companion Volume for Workshop, Tools and Demo papers

September 15 - 19, 2014

Florence, Italy

Acceptance Rates

Overall Acceptance Rate 167 of 463 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
69
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Casaluce RBurattin AChiaromonte FLafuente AVandin A(2024)White-box validation of quantitative product lines by statistical model checking and process miningJournal of Systems and Software10.1016/j.jss.2024.111983210:COnline publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.111983
Kishi T(2023)Family-based Model Checking using Probabilistic Model Checker PRISM2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00048(376-385)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00048
ter Beek MDamiani FLienhardt MMazzanti FPaolini LScarso G(2022)FTS4VMCScience of Computer Programming10.1016/j.scico.2022.102879224:COnline publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102879
Fahrenberg ULegay A(2022)Featured gamesScience of Computer Programming10.1016/j.scico.2022.102874(102874)Online publication date: Sep-2022
https://doi.org/10.1016/j.scico.2022.102874
Beek MMazzanti FDamiani FPaolini LScarso GValfrè MLienhardt MMousavi MSchobbens P(2021)Static analysis and family-based model checking of featured transition systems with VMCProceedings of the 25th ACM International Systems and Software Product Line Conference - Volume B10.1145/3461002.3473071(24-27)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3461002.3473071
Beek MMazzanti FDamiani FPaolini LScarso GLienhardt MMousavi MSchobbens P(2021)Static analysis and family-based model checking with VMCProceedings of the 25th ACM International Systems and Software Product Line Conference - Volume A10.1145/3461001.3472732(214-214)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3461001.3472732
ter Beek MDamiani FLienhardt MMazzanti FPaolini L(2021)Efficient static analysis and verification of featured transition systemsEmpirical Software Engineering10.1007/s10664-020-09930-827:1Online publication date: 23-Oct-2021
https://doi.org/10.1007/s10664-020-09930-8
Ter Beek MLegay ALafuente AVandin A(2020)A Framework for Quantitative Modeling and Analysis of Highly (Re)configurable SystemsIEEE Transactions on Software Engineering10.1109/TSE.2018.285372646:3(321-345)Online publication date: 1-Mar-2020
https://doi.org/10.1109/TSE.2018.2853726
Beek MDamiani FLienhardt MMazzanti FPaolini L(2019)Static Analysis of Featured Transition SystemsProceedings of the 23rd International Systems and Software Product Line Conference - Volume A10.1145/3336294.3336295(39-51)Online publication date: 9-Sep-2019
https://dl.acm.org/doi/10.1145/3336294.3336295
Menghi CSpoletini PChechik MGhezzi C(2019)A verification-driven framework for iterative design of controllersFormal Aspects of Computing10.1007/s00165-019-00484-1Online publication date: 5-Jun-2019
https://doi.org/10.1007/s00165-019-00484-1
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents