PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., De Vink E. P. Towards modular verification of software product lines with mCRL2. In: ISoLA 2014 - Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. 6th International Symposium (Corfu, Greece, 8-11 October 2014). Proceedings, vol. I pp. 368 - 385. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 8802). Springer, 2014.
 
 
Abstract
(English)
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.
URL: http://link.springer.com/chapter/10.1007%2F978-3-662-45234-9_26
DOI: 10.1007/978-3-662-45234-9_26
Subject Product families
Variability
Behavioral analysis
Modular verification
Model checking
mCRL2
D.2.2 Design Tools and Techniques
D.2.4 Software/Program Verification. Formal methods
D.2.4 Software/Program Verification. Model checking
D.2.4 Software/Program Verification. Validation
D.2.13 Reusable Software. Domain engineering


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional