Stefania Gnesi
ABSTRACT
We propose the Controlled Language for Software Product Lines CL4SPL with the twofold aim of ensuring simplicity of use for product line engineers and safe translations to executable languages amenable for automated verification. We show an implementation of CL4SPL in Maude, a well-known rewrite engine, thus allowing formal analyses over product families specified with CL4SPL. We illustrate our approach with a toy family of coffee machines.
- P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. A Logical Framework to Deal with Variability. In IFM'10. LNCS 6396, Springer, 2010, 43--58. Google Scholar
Digital Library
- P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. Formal Description of Variability in Product Families. In SPLC'11. IEEE, 2011, 130--139. Google ScholarDigital Library
- C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google ScholarDigital Library
- 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. Science of Computer Programming 76, 2 (2011), 119--135. Google ScholarDigital Library
- M. H. ter Beek, F. Mazzanti, and A. Sulova. VMC: A Tool for Product Variability Analysis. In FM'12. LNCS 7436, Springer, 2012, 450--454.Google ScholarCross Ref
- A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Model Checking Software Product Lines with SNIP. To appear in Software Tools for Technology Transfer, 2012.Google Scholar
- A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic Model Checking of Software Product Lines. In ICSE'11. ACM, 2011, 321--330. Google ScholarDigital Library
- A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model Checking Lots of Systems. In ICSE'10. ACM, 2010, 335--344. Google ScholarDigital Library
- M. Clavel et al, Eds. All About Maude. LNCS 4350, Springer, 2007.Google Scholar
- D. Fischbein, S. Uchitel, and V. A. Braberman. A Foundation for Behavioural Conformance in Software Product Line Architectures. In ROSATEA'06. ACM, 2006, 39--48. Google ScholarDigital Library
- A. Gondal, M. Poppleton, and M. Butler. Composing Event-B Specifications - Case-Study Experience. In SC'11. LNCS 6708, Springer, 2011, 100--115. Google ScholarDigital Library
- A. Gruler, M. Leucker, and K. D. Scheidemann. Modelling and Model Checking Software Product Lines. In FMOODS'08. LNCS 5051, Springer, 2008, 113--131. Google ScholarDigital Library
- M. Hennessy and R. Milner. On Observing Nondeterminism and Concurrency. In ICALP'80. LNCS 85, Springer, 1980, 299--309. Google ScholarDigital Library
- T. Käkölä and J. C. Dueñas, Eds. Software Product Lines. Springer, 2006.Google ScholarCross Ref
- K. Kang, S. Choen, J. Hess, W. Novak, and S. Peterson. Feature Oriented Domain Analysis (FODA) Feasibility Study. TR SEI-90-TR-21. CMU, 1990.Google Scholar
- K. G. Larsen, U. Nyman, and A. Wąsowski. Modal I/O Automata for Interface and Product Line Theories. In ESOP'07. LNCS 4421, Springer, 2007, 64--79. Google ScholarDigital Library
- K. Lauenroth, K. Pohl, and S. Töhning. Model Checking of Domain Artifacts in Product Line Engineering. In ASE'09. IEEE, 2009, 269--280. Google ScholarDigital Library
- N. Martí-Oliet. An Introduction to Maude and Some of Its Applications. In PADL'10. LNCS 5937, Springer, 2010, 4--9. Google ScholarDigital Library
- I. Matteucci, M. Petrocchi, and M. L. Sbodio. CNL4DSA: a Controlled Natural Language for Data Sharing Agreements. In SAC'10. ACM, 2010, 616--620. Google ScholarDigital Library
- I. Matteucci, M. Petrocchi, M. L. Sbodio, and L. Wiegand. A design phase for data sharing agreements. In DPM'11. LNCS 7122, Springer, 2011, 25--41. Google ScholarDigital Library
- R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google ScholarDigital Library
- R. Muschevici, D. Clarke, and J. Proença. Feature Petri Nets. In FMSPLE'10. Univ. of Lancaster, 2010.Google Scholar
- K. Pohl, G. Böckle, and F. van der Linden. Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, 2005. Google ScholarDigital Library
- C. Stirling. Modal and Temporal Logics for Processes. In 8th Banff Higher Order Workshop 1995. LNCS 1043, Springer, 1996, 149--237. Google ScholarDigital Library
- A. Verdejo and N. Martí-Oliet. Implementing CCS in Maude 2. In WRLA'02. ENTCS 71, 2002, 282--300. Google ScholarDigital Library
- T. Ziadi and J. M. Jézéquel. Product Line Engineering with the UML: Deriving Products. In SPLC'06. Springer, 2006, 557--588.Google Scholar
Index Terms
- Towards an executable algebra for product lines
Recommendations
Combining declarative and procedural views in the specification and analysis of product families
SPLC '13 Workshops: Proceedings of the 17th International Software Product Line Conference co-located workshopsWe introduce the feature-oriented language FLan as a proof of concept for specifying both declarative aspects of product families, namely constraints on their features, and procedural aspects, namely feature configuration and run-time behaviour. FLan is ...
Managing Variability with Traceability in Product and Service Families
HICSS '02: Proceedings of the 35th Annual Hawaii International Conference on System Sciences (HICSS'02)-Volume 3 - Volume 3Service family architectures are based on a set of basic building blocks that can be configured appropriately to build different services based on the same set of assets. These building blocks should be designed to provide variability so as to ...
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 2The 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 ...
Comments