Verification and analysis of variable operating systems
| Autor: | V. V. Kuliamin, E. M. Lavrischeva, V. S. Mutilin, A. K. Petrenko |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Theoretical computer science Computer science Interface (Java) Code coverage покрывающий набор покрытие кода computer.software_genre lcsh:QA75.5-76.95 Domain (software engineering) Conditional compilation General Environmental Science проверка моделей Programming language операционная система Static analysis проверка типов верификация статический анализ семейство систем итеративное уточнение модели на основе контрпримеров модель вариабельности General Earth and Planetary Sciences lcsh:Electronic computers. Computer science computer Software verification System software |
| Zdroj: | Труды Института системного программирования РАН, Vol 28, Iss 3, Pp 189-208 (2018) |
| ISSN: | 2220-6426 2079-8156 |
| DOI: | 10.15514/ispras-2016-28(3)-12 |
| Popis: | This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|