PhD course - Analysis, Test and Verification in The Presence of Variability

Lecturers:
Andrzej Wasowski
Claus Brabrand
Aleksandar Dimovski

Date(s) of the course:
Weekly meetings every Wednesday starting from 5^th February

Time:
9:30 AM-11:00 AM

Room:
4A05 or 3A01

Format:
Research seminar. Presentation and discussion 90 minutes a session, 15 sessions. The course participants are supposed to read the paper before the scheduled discussion slots.

Participants take turns presenting the material. Everybody is expected to actively participate in the discussions.

Program:

• Background (Software Product Lines) [1 session] - (5.02, Stefan)
• Feature Interactions [1 session] (12.02, Tijs)
• Model Checking [2 sessions] (1st session: 19.02, Rao) (2nd session: 26.02, Aleksandar)
• Representation [2 sessions] (1st session: 5.03, Alex) (2nd session: 12.03, Iago)
• Type Checking [2 sessions]
• Static Analysis and Abstract Interpretation [3 sessions]
• Deductive Verification [2 sessions]
• Combinatorial Interaction Testing [1 session]
• Analysis Strategies [1 session]
• Formal Feature Modeling [1 session]

Reading list:

• "On Program Families" by Dijkstra from EWD249.pdf (notes on structured programming)
• David Lorge Parnas: On the Design and Development of Program Families. IEEE Trans. Software Eng. 2(1): 1-9 (1976)
• Christian Prehofer: Feature-oriented programming: A new way of object composition. Concurrency and Computation: Practice and Experience 13(6): 465-501 (2001)
• Pamel Zave's FAQ: http://www2.research.att.com/~pamela/faq.html
• D. Richard Kuhn, Dolores R. Wallace, and Albert M. Gallo. Software fault interactions and implications for software testing. IEEE Transactions on Software Engineering, 30(6):418–421, 2004. [only read sections 1--6]
• Harry C. Li, Shriram Krishnamurthi, Kathi Fisler: Modular Verification of Open Features Using Three-Valued Model Checking. Autom. Softw. Eng. 12(3): 349-382 (2005)
• Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, Jean-François Raskin: Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Software Eng. 39(8): 1069-1089 (2013)
• Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens: Model checking software product lines with SNIP. STTT 14(5): 589-612 (2012) (just this or the above)
• Paul Gazzillo, Robert Grimm: SuperC: parsing all of C by taming the preprocessor. PLDI 2012: 323-334
• Christian Kästner, Paolo G. Giarrusso, Tillmann Rendel, Sebastian Erdweg, Klaus Ostermann, Thorsten Berger: Variability-aware parsing in the presence of lexical macros and conditional compilation. OOPSLA 2011: 805-824
• Martin Erwig and E. Walkingshaw. The choice calculus: A representation for software variation. ACM Trans. Softw. Eng. Methodol., 21(1):6:1–6:27, Dec. 2011
• Christian Kästner, Sven Apel, Thomas Thüm, Gunter Saake: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3): 14 (2012) (or ASE 2008)
• Sheng Chen, Martin Erwig, Eric Walkingshaw: An error-tolerant type system for variational lambda calculus. ICFP 2012: 29-40
• Brabrand, M. Ribeiro, T. Tolêdo, J. Winther, and P. Borba. Intraprocedural dataflow analysis for software product lines. Transactions on Aspect-Oriented Software Development, 10:73–108, 2013.
• Bodden, T. Tolêdo, M. Ribeiro, C. Brabrand, P. Borba, and F. Mezini. SPLLIFT - statically analyzing software product lines in minutes instead of years. In PLDI’13, 2013.
• Midtgaard, J., Brabrand, C. & Wasowski, A. Systematic Derivation of Static Analyses for Software Product Lines. In 2014 ACM SIGPLAN 13th International Conference on MODULARITY. (or its extended version)
• Thomas Thüm, Ina Schaefer, Martin Hentschel, Sven Apel: Family-based deductive verification of software product lines. GPCE 2012: 11-20
• Reiner Hähnle, Ina Schaefer: A Liskov Principle for Delta-Oriented Programming. ISoLA (1) 2012: 32-46 (this or the above, or both in the same session)
• Benjamin Delaware, William R. Cook, Don S. Batory: Product lines of theorems. OOPSLA 2011: 595-608
• Sections from: Feature Interaction: A Critical Review and Considered Forecast. Muffy Calder. Mario Kolberg. Evan H. Magill. Stephan Reiff-Marganiec
• Myra B. Cohen, Matthew B. Dwyer, and Jiangfan Shi. Constructing interaction test suites for highly-configurable systems in the presence of constraints: A greedy approach. IEEE Transactions on Software Engineering, 34:633–650, 2008
• Thomas Thüm, Sven Apel, Christian Kästner, Martin Kuhlemann, Ina Schaefer, and Gunter Saake. Analysis Strategies for Software Product Lines. Technical Report FIN-004-2012, School of Computer Science, University of Magdeburg, Germany, April 2012.
• David Benavides, Sergio Segura and Antonio Ruiz-Cortes. Automated Analysis of Feature Models 20 Years Later: A Literature Review. Journal Information Systems, 615-636.
• Don Batory. Feature models, grammars, and propositional formulas. SPLC 2005, 7-20.
• David Benavides, Pablo Trinidad, and Antonio Ruiz-Cortes. Automated Reasoning on Feature Models. CAiSE 2005, 491–503.

Exam:
Presentation of at least two papers and active participation throughout the seminar is required for passing the course.

Credits:
7.5 ECTS

How to sign up:
Write a mail to adim@itu.dk (Aleksandar Dimovski)

Website:

Can be found here