Верификация и анализ вариабельных операционных систем

В данной работе рассматриваются проблемы верификации и анализа сложных операционных систем с учетом их вариабельности, или наличия большого количества разнообразных конфигураций. Исследуются методы, позволяющие преодолеть эти проблемы, проводится их обзор и классификация. Выделены классы методов, использующих для анализа инструменты, не учитывающие вариабельность, и выборки вариантов системы и методов, использующих специализированные инструменты, учитывающие вариабельность. Как наиболее перспективные с точки зрения масштабируемости, выделены техники анализа, использующие выборки вариантов системы, обеспечивающие покрытие ее кода и комбинаций значений конфигурационных параметров, а также специализированные, учитывающие вариабельность кода техники анализа с итеративным уточнением модели поведения системы на основе контрпримеров.

операционная система, семейство систем, модель вариабельности, верификация, статический анализ, проверка моделей, проверка типов, покрытие кода, покрывающий набор, итеративное уточнение модели на основе контрпримеров

1. Jacobson I., Griss M., Jonsson P. Software Reuse, Architecture, Process and Organization for Business Success. Addison-Wesley, 1997. ISBN-13: 978-0201924763.

2. Bosch J. Design and Use of Software Architectures: Adopting and Evolving a Product Line Approach. Pearson Education, 2000. ISBN-13: 978-0201674941.

3. Clements P., Northrop L. Software Product Lines: Practices and Patterns. SEI Series in Software Engineering, Addison-Wesley, 2001. ISBN-13: 978-0201703320.

4. Pohl K., Böckle G., van der Linden F. J. Software Product Line Engineering: Foundations, Principles and Techniques. Springer-Verlag, 2005. DOI: 10.1007/3-540-28901-1.

5. Bachmann F., Clements P. Variability in software product lines. CMU/SEI Technical Report CMU/SEI-2005-TR-012, 2005.

6. Lotufo R., She S., Berger T., Czarnecki K., Wąsowski A. Evolution of the Linux kernel variability model. Proc. of SPLC’10, LNCS 6287:136-150, Springer, 2010. DOI: 10.1007/978-3-642-15579-6_10.

7. Лаврищева Е. М., Коваль Г.И., Слабоспицькая О.O., Колесник А.Л. Особенности процессов управления при создании семейств программных систем. Проблемы программирования, (3):40-49, 2009.

8. Лаврищева Е.М., Слабоспицькая О.А., Коваль Г.И., Колесник А.А. Теоретические аспекты управления вариабельностью в семействах программных систем. Вестник КНУ, серия физ.-мат. наук, (1):151-158, 2011.

9. Kang K., Cohen S., Hess J., Novak W., Peterson S. Feature-oriented domain analysis (FODA) feasibility study. CMU/SEI Technical Report CMU/SEI-90-TR-21, 1990.

10. Benavides D., Segura S., Ruiz-Cortés A. Automated analysis of feature models 20 years later: a literature review. Information Systems, 35(6):615-636, 2010. DOI: 10.1016/j.is.2010.01.001.

11. Chen L., Babar M.A. A systematic review of evaluation of variability management approaches in software product lines. Information and Software Technology, 53(4):344-362, 2011. DOI: 10.1016/j.infsof.2010.12.006.

12. Berger T., She S., Lotufo R., Wąsowski A., Czarnecki K. A study of variability models and languages in the systems software domain. IEEE Transactions on Software Engineering, 39(12):1611-1640, 2013. DOI: 10.1109/TSE.2013.34.

13. Zippel R. et al. Kconfig language. https://www.kernel.org/doc/Documentation/kbuild/kconfig-language.txt.

14. She S., Berger T. Formal semantics of the Kconfig language. Technical note, University of Waterloo, 2010.

15. Veer B., Dallaway J. The eCos component writer’s guide, 2000.

16. eCos home page. http://ecos.sourceware.org.

17. Berger T., Rublack R., Nair D., Atlee J.M., Becker M., Czarnecki K., Wąsowski A. A survey of variability modeling in industrial practice. Proc. of the 7-th Intl. Workshop on Variability Modelling of Software-intensive Systems (VaMoS’2013), article Νο. 7, ACM 2013. DOI: 10.1145/2430502.2430513.

18. Batory D. Feature models, grammars, and propositional formulas. Proc. of the 9-th Intl. Conf. on Software Product Lines (SPLC’05), LNCS 3714, pp. 7-20, 2005. DOI: 10.1007/11554844_3.

19. Wang H., Li Y., Sun J., Zhang H., Pan J. A semantic web approach to feature modeling and verification. Proc. of Workshop on Semantic Web Enabled Software Engineering (SWESE’05), p. 44, 2005.

20. OWL DL List of reasoners. http://owl.cs.manchester.ac.uk/tools/list-of-reasoners/

21. Haarslev V., Hidde K., Möller R., Wessel M. The RacerPro knowledge representation and reasoning system. Semantic Web, 3(3):267-277, 2012.

22. Benavides D., Segura S., Trinidad P., Ruiz-Cortés A. Using Java CSP solvers in the automated analyses of feature models. Generative and Transformational Techniques in Software Engineering, LNCS 4143:399-408. Springer, 2006. DOI: 10.1007/11877028_16.

23. White J., Doughtery B., Schmidt D., Benavides D. Automated reasoning for multi-step software product-line configuration problems. Proc. of the 13-th Sofware Product Line Conference, pp. 11-20, 2009.

24. Zhang W., Mei H., Zhao H. Feature-driven requirement dependency analysis and high-level software design. Requirements Engineering, 11(3):205-220, 2006. DOI: 10.1007/s00766-006-0033-x.

25. Hemakumar A. Finding Contradictions in Feature Models. Proc. of 12-th Intl. Conf. on Software Product Lines (SPLC’2008), v. 2, pp. 183-190, 2008.

26. Thüm T., Apel S., Kästner C., Kuhlemann M., Schaefer I., Saake G. A classification and survey of analysis strategies for software product lines. ACM Computing Surveys, 47(1), article No. 6, 2014. DOI: 10.1145/2580950.

27. Liebig J., von Rhein A., Kästner C., Apel S., Dörre J., Lengauer C. Scalable analysis of variable software. Proceedings of the 2013 9-th Joint Meeting on Foundations of Software Engineering, pp. 81-91. ACM, 2013. DOI: 10.1145/2491411.2491437.

28. Meinicke J., Thüm T., Schröter R., Benduhn F., Saake G. An overview on analysis tools for software product lines. Proc. of the 18-th Intl. Software Product Line Conf.: Companion Vol. for Workshops, Demonstrations and Tools - Vol. 2, pp. 94-101. ACM, 2014. DOI: 10.1145/2647908.2655972.

29. Dietrich C., Tartler R., Schröder-Preikshat W., Lohmann D. Understanding Linux feature distribution. Proceedings of the 2012 Workshop on Modularity in Systems Software, pp. 15-20. ACM, 2012. DOI: 10.1145/2162024.2162030.

30. Melo J., Flesborg E., Brabrand C., Wąsowski A. A quantitative analysis of variability warnings in Linux. Proceedings of the 10-th International Workshop on Variability Modelling of Software-intensive Systems, pp. 3-8. ACM, 2016. DOI: 10.1145/2866614.2866615.

31. Sayyad A. S., Ingram J., Menzies T., Ammar H. Scalable product line configuration: a straw to break the camel's back. Proc. of IEEE/ACM 28-th International Conference on Automated Software Engineering (ASE 2013), pp. 465-474. IEEE, 2013. DOI: 10.1109/ASE.2013.6693104.

32. Tartler R., Lohmann D., Dietrich C., Egger C., Sincero J. Configuration coverage in the analysis of large-scale system software. SIGOPS Oper. Syst. Rev., 45(3):10-14, 2012. DOI: 10.1145/2039239.2039242.

33. Tartler R., Dietrich C., Sincero J., Schröder-Preikschat W., Lohmann D. Static analysis of variability in system software: the 90000 #ifdefs Issue. Proc. of USENIX Annual Technical Conference (USENIX ATC 14), pp. 421-432, 2014.

34. Sloane N.J.A. Covering arrays and intersecting codes. Journal of combinatorial designs, 1(1):51-63, 1993. DOI: 10.1002/jcd.3180010106.

35. Hartman A., Raskin L. Problems and algorithms for covering arrays. Discrete Mathematics, 284(1):149-156, 2004. DOI: 10.1016/j.disc.2003.11.029.

36. Кулямин В.В., Петухов А.А. Обзор методов построения покрывающих наборов. Программирование 37(3):3-41, 2011. DOI: 10.1134/S0361768811030029.

37. Cohen M.B., Gibbons P.B., Mugridge W.B., Colbourn C.J. Constructing test suites for interaction testing. Proc. of 25-th Intl. Conf. on Software Engineering, pp. 38-48. IEEE, 2003. DOI: 10.1109/ICSE.2003.1201186.

38. Grindal M., Offutt A.J., Andler S.F. Combination testing strategies: a survey. Software Testing, Verification, and Reliability, 15(3):167-199, 2005. DOI: 10.1002/stvr.319.

39. Perrouin G., Oster S., Sen S., Klein J., Baudry B., Le Traon Y. Pairwise testing for software product lines: comparison of two approaches. Software Quality Journal, 20(3-4):605-643, 2012. DOI: 10.1007/s11219-011-9160-9.

40. Johansen M.F., Haugen Ø, Fleurey F. Properties of realistic feature models make combinatorial testing of product lines feasible. Proc. of Intl. Conf. on Model Driven Engineering Languages and Systems, pp. 638-652. Springer, 2011. DOI: 10.1007/978-3-642-24485-8_47.

41. Кулямин В.В. Комбинаторная генерация программных конфигураций ОС. Труды ИСП РАН, 23:359-370, 2012. DOI: 10.15514/ISPRAS-2012-23-20.

42. Brabrand C., Ribeiro M., Tolêdo T., Borba P. Intraprocedural dataflow analysis for software product lines. Proc. Intl. Conf. on Aspect-Oriented Software Development (AOSD), pp. 13-24. ACM, 2012. DOI: 10.1007/978-3-642-36964-3_3.

43. Thaker S., Batory D., Kitchin D., Cook W. Safe composition of product lines. Proc. of Intl. Conf. on Generative Programming and Component Engineering (GPCE), pp. 95-104. ACM, 2007. DOI: 10.1145/1289971.1289989.

44. Heidenreich F. Towards systematic ensuring well-formedness of software product lines. Proc. of Intl. Workshop on Feature-Oriented Software Development (FOSD), pp. 69-74. ACM, 2009. DOI: 10.1145/1629716.1629730.

45. Apel S., Kästner C., Größlinger A., Lengauer C. Type safety for feature-oriented product lines. Automated Software Engineering, 17(3):251-300, 2010. DOI: 10.1007/s10515-010-0066-8.

46. Kästner C., Apel S., Thüm T., Saake G. Type checking annotation-based product lines. ACM Trans. Software Engineering and Methodology, 21(3):1-39, 2012. DOI: 10.1145/2211616.2211617.

47. Gruler A., Leucker M., Scheidemann K. Modeling and model checking software product lines. Proc. of IFIP Intl. Conf. on Formal Methods for Open Object-based Distributed Systems (FMOODS), pp. 113-131. Springer, 2008. DOI: 10.1007/978-3-540-68863-1_8.

48. Lauenroth K., Toehning S., Pohl K. Model checking of domain artifacts in product line engineering. Proc. Intl. Conf. on Automated Software Engineering (ASE), pp. 269-280. IEEE, 2009. DOI: 10.1109/ASE.2009.16.

49. 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. Proc. Int. Conf. Software Engineering (ICSE), pp. 335-344. ACM, 2010. DOI: 10.1145/1806799.1806850.

50. Apel S., Speidel H., Wendler P., von Rhein A., Beyer D. Detection of feature interactions using feature-aware verification. Proc. of Intl. Conf. on Automated Software Engineering (ASE), pp. 372-375. IEEE, 2011. DOI: 10.1109/ASE.2011.6100075.

51. Cordy M., Heymans P., Legay A., Schobbens P.-Y., Dawagne B., Leucker M. Counterexample guided abstraction refinement of product-line behavioural models. Proc. of 22-nd ACM SIGSOFT Intl. Symposium on Foundations of Software Engineering (FSE 2014), pp. 190-201. ACM, 2014. DOI: 10.1145/2635868.2635919.

52. Thüm T., Schaefer I., Apel S., Hentschel M. Family-based deductive verification of software product lines. Proc. of the 11-th Intl. Conf. on Generative Programming and Component Engineering (GPCE '12), pp. 11-20. ACM, 2012. DOI: 10.1145/2371401.2371404.

53. Kästner C., von Rhein A., Erdweg S., Pusch J., Apel S., Rendel T., Ostermann K. Toward variability-aware testing. Proc. of Intl. Workshop on Feature-Oriented Software Development (FOSD), pp. 1-8. ACM, 2012. DOI: 10.1145/2377816.2377817.