A logical framework to deal with variability
Asirelli P., Ter Beek M. H., Fantechi A., Gnesi S.
Product family Modal Transition Systems Variability ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.2: Design Tools and Techniques Software Product Families Deontic Logic Temporal logic [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Deontic logic ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.1: Requirements/Specifications Product families ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Variability modeling
We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy-Milner logic with Until and we interpret it over Modal Transition Systems (MTSs). MTSs extend the classical notion of Labelled Transition Systems by distinguishing possible (may) and required (must) transitions: these two types of transitions are useful to describe variability in behavioural descriptions of product families. This leads to a novel deontic interpretation of the classical modal and temporal operators, which allows the expression of both constraints over the products of a family and constraints over their behaviour in a single logical framework. Finally, we sketch model-checking algorithms to verify MHML formulae as well as a way to derive correct products from a product family description.
Source: Lecture notes in computer science 6396 (2010): 43–58. doi:10.1007/978-3-642-16265-7_5
Publisher: Springer, Berlin , Germania
2. Åqvist, L.: Deontic Logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 8, pp. 147-264. Kluwer, Dordrecht (2002)
3. Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: Deontic Logics for modelling Behavioural Variability. In: Benavides, D., Metzger, A., Eisenecker, U. (eds.) Proceedings Variability Modelling of Software-intensive Systems (VaMoS 2009). ICB Research Report, vol. 29, pp. 71-76. Universität Duisburg, Essen (2009)
4. Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A deontic logical framework for modelling product families. In: Benavides, D., Batory, D., Grünbacher, P. (eds.) Proceedings Variability Modelling of Software-intensive Systems (VaMoS 2010). ICB Research Report, vol. 37, pp. 37-44. Universität Duisburg, Essen (2010)
5. Batory, D.: Feature Models, Grammars and Propositional Formulas. In: Obbink, H., Pohl, K. (eds.) SPLC 2005. LNCS, vol. 3714, pp. 7-20. Springer, Heidelberg (2005)
6. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action/state-based modelchecking approach for the analysis of communication protocols for service-oriented applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 133-148. Springer, Heidelberg (2008)
7. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based modelchecking approach for the analysis of abstract system properties. Sci. Comput. Program. (to appear 2010)
8. Castro, P.F., Maibaum, T.S.E.: A Complete and Compact Propositional Deontic Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 109-123. Springer, Heidelberg (2007)
9. Castro, P.F., Maibaum, T.S.E.: A Tableaux System for Deontic Action Logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 34-48. Springer, Heidelberg (2008)
10. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 8(2), 244-263 (1986)
11. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT, Cambridge (1999)
12. Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In: Proceedings 32nd ACM/IEEE International Conference on Software Engineering, vol. 1, pp. 335-344. ACM, New York (2010)
13. Czarnecki, K., Eisenecker, U.W.: Generative Programming: Methods, Tools, and Applications. Addison-Wesley, Boston (2000)
14. De Nicola, R., Vaandrager, F.W.: Three Logics for Branching Bisimulation. J. ACM 42(2), 458-487 (1995)
15. D'Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: The Modal Transition System Analyser. In: Proceedings 23rd IEEE/ACM International Conference on Automated Software Engineering, pp. 475-476. IEEE, Washington (2008)
16. Fantechi, A., Gnesi, S.: A Behavioural Model for Product Families. In: Crnkovic, I., Bertolino, A. (eds.) Proceedings 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT symposium on Foundations of Software Engineering, pp. 521-524. ACM, New York (2007)
17. Fantechi, A., Gnesi, S.: Formal modelling for Product Families Engineering. In: Proceedings 12th International Software Product Line Conference, pp. 193-202. IEEE, Washington (2008)
18. Fantechi, A., Gnesi, S., Lami, G., Nesti, E.: A Methodology for the Derivation and Verification of Use Cases for Product Lines. In: Nord, R.L. (ed.) SPLC 2004. LNCS, vol. 3154, pp. 255-265. Springer, Heidelberg (2004)
19. Fischbein, D., Uchitel, S., Braberman, V.A.: A Foundation for Behavioural Conformance in Software Product Line Architectures. In: Hierons, R.M., Muccini, H. (eds.) Proceedings ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, pp. 39-48. ACM, New York (2006)
20. Gruler, A., Leucker, M., Scheidemann, K.D.: Modelling and Model Checking Software Product Lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113-131. Springer, Heidelberg (2008)
21. Gruler, A., Leucker, M., Scheidemann, K.D.: Calculating and Modelling Common Parts of Software Product Lines. In: Proceedings 12th International Software Product Line Conference, pp. 203-212. IEEE, Washington (2008)
22. Kang, K., Choen, S., Hess, J., Novak, W., Peterson, S.: Feature Oriented Domain Analysis (FODA) Feasibility Study. Technical Report SEI-90-TR-21, Carnegie Mellon University (1990)
23. Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 232-246. Springer, Heidelberg (1989)
24. Larsen, K.G.: Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion. Theor. Comput. Sci. 72(2-3), 265-288 (1990)
25. Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O Automata for Interface and Product Line Theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64-79. Springer, Heidelberg (2007)
26. Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proceedings 3rd Annual Symposium on Logic in Computer Science, pp. 203-210. IEEE, Washington (1988)
27. Mannion, M., Camara, J.: Theorem Proving for Product Line Model Verification. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 211-224. Springer, Heidelberg (2004)
28. Mazzanti, F.: UMC model checker v3.6 (2009), http://fmt.isti.cnr.it/umc
29. Meyer, J.-J.C., Wieringa, R.J. (eds.): Deontic Logic in Computer Science: Normative System Specification. John Wiley & Sons, Chichester (1994)
30. Meyer, M.H., Lehnerd, A.P.: The Power of Product Platforms: Building Value and Cost Leadership. The Free Press, New York (1997)
31. Müller-Olm, M., Schmidt, D.A., Steffen, B.: Model-Checking: A Tutorial Introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330-354. Springer, Heidelberg (1999)
32. Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering: Foundations, Principles and Techniques. Springer, Heidelberg (2005)
33. Schmidt, H., Fecher, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebraic Program. 77(1-2), 20-39 (2008)
Metrics
Back to previous page
@article{oai:it.cnr:prodotti:44235,
title = {A logical framework to deal with variability},
author = {Asirelli P. and Ter Beek M. H. and Fantechi A. and Gnesi S.},
publisher = {Springer, Berlin , Germania},
doi = {10.1007/978-3-642-16265-7_5},
journal = {Lecture notes in computer science},
volume = {6396},
pages = {43–58},
year = {2010}
}
0000-0002-4648-4667DOIAlso available from
Flore (Florence Research Repository)
Hyper Article en Ligne
www.springerlink.com