Efficient static analysis and verification of featured transition systems
| العنوان: | Efficient static analysis and verification of featured transition systems |
|---|---|
| المؤلفون: | Franco Mazzanti, Maurice H. ter Beek, Luca Paolini, Michael Lienhardt, Ferruccio Damiani |
| المصدر: | Empirical software engineering (Online) 27 (2022). doi:10.1007/s10664-020-09930-8 info:cnr-pdr/source/autori:ter Beek M.H.; Damiani F.; Lienhardt M.; Mazzanti F.; Paolini L./titolo:Efficient static analysis and verification of featured transition systems/doi:10.1007%2Fs10664-020-09930-8/rivista:Empirical software engineering (Online)/anno:2022/pagina_da:/pagina_a:/intervallo_pagine:/volume:27 |
| بيانات النشر: | Kluwer, Dordrecht , Paesi Bassi, 2022. |
| سنة النشر: | 2022 |
| مصطلحات موضوعية: | Model checking, Behavioural model, Computer science, Software product lines, Static analysis, Deadlock, Featured transition systems, Formal verification, Product (mathematics), Transition system, Redundancy (engineering), Benchmark (computing), Formal specification, Software product line, Algorithm, Software |
| الوصف: | A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification—if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs. |
| اللغة: | English |
| DOI: | 10.1007/s10664-020-09930-8 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::aff399b0783eef5849edbc716de8c6c9 https://openportal.isti.cnr.it/doc?id=people______::b0fc0a1e270d834c9f969267700c3a48 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....aff399b0783eef5849edbc716de8c6c9 |
| قاعدة البيانات: | OpenAIRE |
| DOI: | 10.1007/s10664-020-09930-8 |
|---|