Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

You searched for +publisher:"DIAL (Belgium)" +contributor:("Greenyer, Joel"). One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Cordy, Maxime. Model Checking for the Masses.

Degree: 2014, DIAL (Belgium)

The model-checking problem for software product lines is harder than for single systems. Indeed, one has to verify all the software variants of a product line, whose number grows exponentially in the number of their differences. Techniques intended for single systems are inefficient in this case, for these can only be applied to all products separately. Variability-aware modelling formalisms and algorithms were designed as a more appropriate answer to that problem. Their strength lies in their ability to check a behaviour common to several products only once, which leads to substantial performance gains. Although they constitute a major step toward the efficient verification of product lines, these techniques are not yet mature enough to truly achieve this objective. They still lack optimisations to verify large models, the expressiveness to represent complex forms of variable behaviour, as well as usable languages and tools required for industrial transfer. This thesis aims at improving product-line model checking in order to provide formalisms, algorithms, and tools that together hold the potential to verify real-world software product lines. We first study the state-of-the-art model-checking approaches for software product lines. We compare them in terms of available formalisms and algorithms, and we determine that the approach based on Featured Transition Systems (FTS) is the most suitable to act as a basis for the design of novel techniques. We then extend its theory along two axes: efficiency and expressiveness. For the former, we propose abstraction methods that can reduce the size of the model to check while maintaining correctness and completeness; they consist of extensions of single-system abstraction techniques applied to FTS, and of new techniques that abstract away from their variability. As for expressiveness, on the one hand we propose featured timed automata as a combination of FTS and real-time behaviour. On the other hand, we analyse how to support in FTS complex forms of variability such as numeric features and multi-features. We implemented our theoretical results into a new model-checking tool named ProVeLines. As all our extensions are based on FTS, they share many commonalities. ProVeLines was therefore designed as a product line whose each variant implements a distinct combination of verification formalisms and algorithms. Finally, we show that the principles we designed for product-line model checking can also be applied to other formal methods, namely the verification of adaptive systems and the synthesis of controllers for product lines.

(DOCSC06)  – UNamur, 2014

Advisors/Committee Members: UNamur - INF_PRECISE, UNamur - Ecole doctorale en sciences, Atlee, Joanne, Greenyer, Joel, Heymans, Patrick, Legay, Axel, Petit, Michaël, Schobbens, Pierre-Yves.

Subjects/Keywords: Formal methods; model checking; software product lines

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Cordy, M. (2014). Model Checking for the Masses. (Thesis). DIAL (Belgium). Retrieved from http://hdl.handle.net/2078.2/152729

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16th Edition):

Cordy, Maxime. “Model Checking for the Masses.” 2014. Thesis, DIAL (Belgium). Accessed May 22, 2019. http://hdl.handle.net/2078.2/152729.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7th Edition):

Cordy, Maxime. “Model Checking for the Masses.” 2014. Web. 22 May 2019.

Vancouver:

Cordy M. Model Checking for the Masses. [Internet] [Thesis]. DIAL (Belgium); 2014. [cited 2019 May 22]. Available from: http://hdl.handle.net/2078.2/152729.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Cordy M. Model Checking for the Masses. [Thesis]. DIAL (Belgium); 2014. Available from: http://hdl.handle.net/2078.2/152729

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

.