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:("Berthomieu, Bernard"). Showing records 1 – 3 of 3 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Peres, Florent. Réseaux de Petri temporels à inhibitions / permissions : application à la modélisation et vérification de systèmes de tâches temps réel : Forbid/Allow time Petri nets – Application to the modeling and checking of real time tasks systems.

Degree: Docteur es, Sureté du logiciel et calcul à haute performance, 2010, Toulouse, INSA

Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour lasécurité : ils en contrôlent l’exécution afin que celles-ci se comportent de manière sûre dans le contexte d’un environnement dont l’évolution peut être imprévisible. Un STR n’a d’autre alternative que de s’adapter à son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier.Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté àla description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelquestˆaches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe.En premier lieu, la modélisation efficace d’une gamme étendue de politiques d’ordonnancementsse heurte à l’incapacité des RdPT à imposer un ordre d’apparition à des évènements concurrentssurvenant au même instant. D’autre part, les STR ont une nette tendance à être constitués de caractéristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guèreadaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deuxproblèmes, nous proposons dans cette thèse Cifre – en partenariat entre Airbus et le Laas-Cnrs– d’étendre les RdPT à l’aide de deux nouvelles relations, les relations d’inhibition et de permission,permettant de spécifier de manière plus fine les contraintes de temps.Afin de cerner un périmètre clair d’adéquation de cette nouvelle extension à la modélisation dessystèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs :déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporelsà inhibitions/permissions et fournir un langage simple à la communauté temps réel dont lavérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L’explorateur d’espace d’états de laboite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola

Real time systems (RTS) are at the core of safety critical devices : they control thedevices’ behavior in such a way that they remain safe with regard to an unpredictable environment. ARTS has no other choices than to adapt to its environment : its correctness depends upon its responsetime to the stimuli stemming from the environment.It is widely accepted that the Time Petri nets (TPN) formalism is adapted to the description ofRTS. However, the modeling of simple systems with only a few periodic tasks scheduled according toa basic policy remains a challenge in the worst case and can be very tedious in the most favorable one.First, we put forward some limitations of TPN regarding the modeling of a wide variety of schedulingpolicies, coming from the fact that this formalism is not always capable to impose a givenorder on events whenever they happen at the same time. Moreover, RTS are usually constituted of thesame recurring features, implying a compositional modeling,…

Advisors/Committee Members: Vernadat, François B. (thesis director), Berthomieu, Bernard (thesis director).

Subjects/Keywords: Systèmes temps réel; Model checking; Réseau de Petri temporel; Angage spécifique à un domaine; Domain specific language; Real time systems; Model checking; Time Petri nets

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Peres, F. (2010). Réseaux de Petri temporels à inhibitions / permissions : application à la modélisation et vérification de systèmes de tâches temps réel : Forbid/Allow time Petri nets – Application to the modeling and checking of real time tasks systems. (Doctoral Dissertation). Toulouse, INSA. Retrieved from http://www.theses.fr/2010ISAT0004

Chicago Manual of Style (16th Edition):

Peres, Florent. “Réseaux de Petri temporels à inhibitions / permissions : application à la modélisation et vérification de systèmes de tâches temps réel : Forbid/Allow time Petri nets – Application to the modeling and checking of real time tasks systems.” 2010. Doctoral Dissertation, Toulouse, INSA. Accessed January 19, 2020. http://www.theses.fr/2010ISAT0004.

MLA Handbook (7th Edition):

Peres, Florent. “Réseaux de Petri temporels à inhibitions / permissions : application à la modélisation et vérification de systèmes de tâches temps réel : Forbid/Allow time Petri nets – Application to the modeling and checking of real time tasks systems.” 2010. Web. 19 Jan 2020.

Vancouver:

Peres F. Réseaux de Petri temporels à inhibitions / permissions : application à la modélisation et vérification de systèmes de tâches temps réel : Forbid/Allow time Petri nets – Application to the modeling and checking of real time tasks systems. [Internet] [Doctoral dissertation]. Toulouse, INSA; 2010. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2010ISAT0004.

Council of Science Editors:

Peres F. Réseaux de Petri temporels à inhibitions / permissions : application à la modélisation et vérification de systèmes de tâches temps réel : Forbid/Allow time Petri nets – Application to the modeling and checking of real time tasks systems. [Doctoral Dissertation]. Toulouse, INSA; 2010. Available from: http://www.theses.fr/2010ISAT0004

2. 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 19, 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. 19 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 19]. 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

3. Bourdil, Pierre-Alain. Contribution à la modélisation et la vérification formelle par model checking - Symétries pour les Réseaux de Petri temporels : Contribution to the modeling and formal verification by model checking - Symmetries for Temporal Petri Nets.

Degree: Docteur es, Sûreté de Logiciel et Calcul de Haute Performance, 2015, Toulouse, INSA

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés.

This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

Advisors/Committee Members: Vernadat, François B. (thesis director), Berthomieu, Bernard (thesis director), Jenn, Éric (thesis director).

Subjects/Keywords: Réseaux de Petri Temporels; Symétries; Modélisation formelle; Vérification formelle; Avionique; Model-Checking; Time Petri Net; Symmetry; Formal modeling; Avionics; 510; 004

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bourdil, P. (2015). Contribution à la modélisation et la vérification formelle par model checking - Symétries pour les Réseaux de Petri temporels : Contribution to the modeling and formal verification by model checking - Symmetries for Temporal Petri Nets. (Doctoral Dissertation). Toulouse, INSA. Retrieved from http://www.theses.fr/2015ISAT0041

Chicago Manual of Style (16th Edition):

Bourdil, Pierre-Alain. “Contribution à la modélisation et la vérification formelle par model checking - Symétries pour les Réseaux de Petri temporels : Contribution to the modeling and formal verification by model checking - Symmetries for Temporal Petri Nets.” 2015. Doctoral Dissertation, Toulouse, INSA. Accessed January 19, 2020. http://www.theses.fr/2015ISAT0041.

MLA Handbook (7th Edition):

Bourdil, Pierre-Alain. “Contribution à la modélisation et la vérification formelle par model checking - Symétries pour les Réseaux de Petri temporels : Contribution to the modeling and formal verification by model checking - Symmetries for Temporal Petri Nets.” 2015. Web. 19 Jan 2020.

Vancouver:

Bourdil P. Contribution à la modélisation et la vérification formelle par model checking - Symétries pour les Réseaux de Petri temporels : Contribution to the modeling and formal verification by model checking - Symmetries for Temporal Petri Nets. [Internet] [Doctoral dissertation]. Toulouse, INSA; 2015. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2015ISAT0041.

Council of Science Editors:

Bourdil P. Contribution à la modélisation et la vérification formelle par model checking - Symétries pour les Réseaux de Petri temporels : Contribution to the modeling and formal verification by model checking - Symmetries for Temporal Petri Nets. [Doctoral Dissertation]. Toulouse, INSA; 2015. Available from: http://www.theses.fr/2015ISAT0041

.