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:

Sorted by: relevance · author · university · dateNew search

You searched for +publisher:"Toulouse, INSA" +contributor:("Dal Zilio, Silvano"). Showing records 1 – 2 of 2 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Tacla Saad, Rodrigo. Parallel model checking for multiprocessor architecture : Model checking sur architecture multiprocesseur.

Degree: Docteur es, Sûreté de logiciel et calcul de haute performance, 2011, Toulouse, INSA

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérification formelle de systèmes réactifs finis sur architectures parallèles. Ces travaux se basent sur les techniques de vérification model checking. Notre approche cible des architectures multi-processeurs et multi-cœurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement.Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois efficaces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d’espaces d'états en parallèle; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs.Parallèlement à la définition de nouveaux algorithmes de model checking pour machines multi-cœurs, nous nous intéressons également aux algorithmes de vérification probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérification d’un système. La vérification probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d’une faible probabilité de ne pas être exhaustif; il s’agit donc d’une stratégie permettant de répondre au problème de l’explosion combinatoire

In this thesis, we propose and study new algorithms and data structures for model checking finite-state, concurrent systems. We focus on techniques that target shared memory, multi-cores architectures, that are a current trend in computer architectures.In this context, we present new algorithms and data structures for exhaustive parallel model checking that are as efficient as possible, but also ``friendly'' with respect to the work-sharing policies that are used for the state space generation (e.g. a work-stealing strategy): at no point do we impose a restriction on the way work is shared among the processors. This includes both the construction of the state space as the detection of cycles in parallel, which is is one of the key points of performance for the evaluation of more complex formulas.Alongside the definition of enumerative, model checking algorithms for many-cores architectures, we also study probabilistic verification algorithms. By the term probabilistic, we mean that, during the exploration of a system, any given reachable state has a high probability of being checked by the algorithm. Probabilistic verification trades savings at the level of memory usage for the probability of missing some states. Consequently, it becomes possible to analyze part of the state space of a system when there is not enough memory available to represent the entire state space in an exact manner

Advisors/Committee Members: Berthomieu, Bernard (thesis director), Dal Zilio, Silvano (thesis director).

Subjects/Keywords: Model Checking en Parallèle; Vérification Formelle et Logiques Temporelles; Algorithme et Structure de Données concurrents; Méthode Formelle; Parallel Model Checking; Concurrent algorithms and data structures; Formal Verification and Temporal Logic; Formal Methods

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Tacla Saad, R. (2011). Parallel model checking for multiprocessor architecture : Model checking sur architecture multiprocesseur. (Doctoral Dissertation). Toulouse, INSA. Retrieved from http://www.theses.fr/2011ISAT0028

Chicago Manual of Style (16th Edition):

Tacla Saad, Rodrigo. “Parallel model checking for multiprocessor architecture : Model checking sur architecture multiprocesseur.” 2011. Doctoral Dissertation, Toulouse, INSA. Accessed January 28, 2020. http://www.theses.fr/2011ISAT0028.

MLA Handbook (7th Edition):

Tacla Saad, Rodrigo. “Parallel model checking for multiprocessor architecture : Model checking sur architecture multiprocesseur.” 2011. Web. 28 Jan 2020.

Vancouver:

Tacla Saad R. Parallel model checking for multiprocessor architecture : Model checking sur architecture multiprocesseur. [Internet] [Doctoral dissertation]. Toulouse, INSA; 2011. [cited 2020 Jan 28]. Available from: http://www.theses.fr/2011ISAT0028.

Council of Science Editors:

Tacla Saad R. Parallel model checking for multiprocessor architecture : Model checking sur architecture multiprocesseur. [Doctoral Dissertation]. Toulouse, INSA; 2011. Available from: http://www.theses.fr/2011ISAT0028

2. Abid, Nouha. Verification of real time properties in Fiacre language : Vérification des propriétés temps réel dans le langage Fiacre.

Degree: Docteur es, Sûreté logicielle et calcul de haute performance, 2012, Toulouse, INSA

Dans cette thèse, nous nous intéressons à la problématique de la vérification formelle des systèmes critiques temps réel, c’est-à-dire des systèmes dont l’exécution dépend de certaines contraintes temporelles. La spécification formelle des exigences pour de tels systèmes, ainsi que leur vérification, reste une tâche très compliquée, surtout pour les non experts. Plusieurs solutions ont été proposées pour faciliter la spécification et la vérification des systèmes temps-réels. Un premier type d’approche est basée sur la définition d’un ensemble de patrons de spécification qui représentent les propriétés les plus utilisées en pratique. Cependant, ce type de solutions n’est pas toujours supporté par un outillage de vérification efficace, dans le sens que les auteurs de ces langages de patrons ne fournissent pas directement une implantation pour leur langage. Un second type d’approches repose sur l’utilisation du formalisme des logiques temporelles pour spécifier les propriétés à vérifier et sur les techniques de model-checking pour leur vérification. S’agissant de systèmes temps-réels, il est dans ce cas nécessaire d’utiliser des extensions temporisées des logiques temporelles. Cependant, ces approches donnent le plus souvent lieu à des problèmes de model-checking qui sont indécidable, ou dont la complexité en pratique est très élevée. Dans ce travail, nous suivons la première approche et proposons un langage de patrons de propriétés temps-réels accompagnés d’un outil de vérification par model- checking. Nous apportons plusieurs contributions à ce domaine. Nous proposons un cadre théorique complet pour la spécification et la vérification de patrons de propriétés temps réel. Notre approche a été implantée dans le contexte du langage de modélisation Fiacre. Enfin, nous définissons deux méthodes complémentaires permettant de vérifier la correction de notre approche de vérification

The formal verification of critical, reactive systems is a very complicated task, especially for non experts. In this work, we more particularly address the problem of real time systems, that is in the situation where the correctness of the system depends upon timing constraints, such as the “timeliness” of some interactions. Many solutions have been proposed to ease the specification and the verification of such systems. An interesting approach—that we follow in this thesis—is based on the definition of specification patterns, that is sets of general, reusable templates for commonly occurring classes of properties. However, patterns are rarely implemented, in the sense that the designers of specification languages rarely provide an effective verification method for checking a pattern on a system. The most common technique is to rely on a timed extension of a temporal logic to define the semantics of patterns and then to use a model-checker for this logic. However, this approach may be inadequate, in particular if patterns require the use of a logic associated to an undecidable model-checking problem or to an algorithm with a very high…

Advisors/Committee Members: Vernadat, François B. (thesis director), Dal Zilio, Silvano (thesis director), Le botlan, Didier (thesis director).

Subjects/Keywords: Vérification formelle; Systèmes temps réel; Langage d’exigences; Patron de spécification; Model-checking; Observateurs; Verification; Requirement; Specification Patterns; Model Checking; Observers; Real Time Systems; 005.8

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Abid, N. (2012). Verification of real time properties in Fiacre language : Vérification des propriétés temps réel dans le langage Fiacre. (Doctoral Dissertation). Toulouse, INSA. Retrieved from http://www.theses.fr/2012ISAT0033

Chicago Manual of Style (16th Edition):

Abid, Nouha. “Verification of real time properties in Fiacre language : Vérification des propriétés temps réel dans le langage Fiacre.” 2012. Doctoral Dissertation, Toulouse, INSA. Accessed January 28, 2020. http://www.theses.fr/2012ISAT0033.

MLA Handbook (7th Edition):

Abid, Nouha. “Verification of real time properties in Fiacre language : Vérification des propriétés temps réel dans le langage Fiacre.” 2012. Web. 28 Jan 2020.

Vancouver:

Abid N. Verification of real time properties in Fiacre language : Vérification des propriétés temps réel dans le langage Fiacre. [Internet] [Doctoral dissertation]. Toulouse, INSA; 2012. [cited 2020 Jan 28]. Available from: http://www.theses.fr/2012ISAT0033.

Council of Science Editors:

Abid N. Verification of real time properties in Fiacre language : Vérification des propriétés temps réel dans le langage Fiacre. [Doctoral Dissertation]. Toulouse, INSA; 2012. Available from: http://www.theses.fr/2012ISAT0033

.