Retour au site du LAAS-CNRS

Laboratoire d’analyse et d’architecture des systèmes
Choisir la langue : FR | EN

4documents trouvés

16510
21/11/2016

Contribution à la conception et à la vérification de systèmes temps réel - Focus sur l'ordonnancement temps réel

P.E.HLADIK

VERTICS

Habilitation à diriger des recherches : 21 Novembre 2016, 153p., Président: J.C.FABRE, Rapporteurs: L.GEORGE, E.GROLLEAU, G.LIPARI, Examinateurs: N.NAVET, F.SINGHOFF , N° 16510

Lien : https://hal.archives-ouvertes.fr/tel-01451027

Diffusable

Plus d'informations

Résumé

Cette Habilitation à Diriger les Recherches est l'occasion de présenter mes travaux de recherche sur la conception et la validation des systèmes embarqués critiques. Après une introduction du contexte de recherche, l'exposé se focalisera sur les problématiques de l’ordonnancement temps réel et sur les diverses problématiques que j'ai pu aborder dans ce contexte. Une attention particulière sera portée à la configuration d'architectures avioniques ainsi qu’à l'évaluation des politiques d'ordonnancement multiprocesseur pour l'automobile. L’exposé se conclura sur les perspectives envisagées pour poursuivre ces travaux et les étendre à la génération d’exécutable temporellement fiable.

Mots-Clés / Keywords
Conception; Ordonnancement; Système embarqué; Temps réel; Validation;

138933
15675
03/12/2015

Contribution à la modélisation et la vérification formelle par model-checking - Symétries pour les Réseaux de Petri Temporels

P.A.BOURDIL

VERTICS

Doctorat : INSA de Toulouse, 3 Décembre 2015, 148p., Président: J.P.BODEVEIX, Rapporteurs: B.BERARD, P.MOREAUX, Examinateurs: E.JENN, D.LIME, L.PETRUCCI, Directeurs de thèse: F.VERNADAT, B.BERTHOMIEU , N° 15675

Lien : https://tel.archives-ouvertes.fr/tel-01291834

Diffusable

Plus d'informations

Abstract

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.

Résumé

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.

136309
14571
11/12/2014

Étude et évaluation des politiques d'ordonnancement temps réel multiprocesseur

M.CHERAMY

VERTICS

Doctorat : INSA de Toulouse, 11 Décembre 2014, 228p., Président: J.C.FABRE, Rapporteurs: L.CUCU-GROSJEAN, P.RICHARD, Examinateur: Y.TRINQUET, Directeurs de thèse: P.E.HLADIK, A.M.DEPLANCHE , N° 14571

Lien : https://tel.archives-ouvertes.fr/tel-01104953

Diffusable

Plus d'informations

Abstract

Numerous algorithms have been proposed to address the scheduling of real-time tasks for multiprocessor architectures. Yet, new scheduling algorithms have been defined very recently. Therefore, and without any guarantee of completeness, we have identified more than fifty of them. This large diversity makes the comparison of their behavior and performance difficult. This research aims at allowing the study and the evaluation of key scheduling algorithms. The first contribution is SimSo, a new simulation tool dedicated to the evaluation of scheduling algorithms. Using this tool, we were able to compare the performance of twenty algorithms. The second contribution is the consideration, in the simulation, of temporal overheads related to the execution of the scheduler and the impact of memory caches on the computation time of the jobs. This is done by the introduction of statistical models evaluating the cache miss ratios.

Résumé

De multiples algorithmes ont été proposés pour traiter de l’ordonnancement de tâches temps réel dans un contexte multiprocesseur. Encore très récemment de nouvelles politiques ont été définies. Ainsi, sans garantie d’exhaustivité, nous en avons recensé plus d’une cinquantaine. Cette grande diversité rend difficile une analyse comparée de leurs comportements et performances. L’objectif de ce travail de thèse est de permettre l’étude et l’évaluation des principales politiques d’ordonnancement existantes. La première contribution est SimSo, un nouvel outil de simulation dédié à l’évaluation des politiques. Grâce à cet outil, nous avons pu comparer les performances d’une vingtaine d’algorithmes. La seconde contribution est la prise en compte, dans la simulation, des surcoûts temporels liés à l’exécution du code de l’ordonnanceur et à l’influence des mémoires caches sur la durée d’exécution des travaux par l’introduction de modèles statistiques évaluant les échecs d’accès à ces mémoires.

Mots-Clés / Keywords
Temps-réel; Multiprocesseur; Multicoeur; Évaluation; Cache; Scheduling; Real-time; Multiprocessor; Multicore; Evaluation; Ordonnancement;

133774
12749
11/12/2012

Verification of real time properties in fiacre language

N.ABID

VERTICS

Doctorat : INSA de Toulouse, 11 Décembre 2012, 157p., Président: Y.AIT AMEUR, Rapporteurs: O.H.ROUX, F.SIMONOT-LION, Examinateurs: O.LAURENT, D.LE BOTLAN, Directeurs de thèse: F.VERNADAT, S.DAL ZILIO , N° 12749

Lien : http://tel.archives-ouvertes.fr/tel-00782554

Diffusable

Plus d'informations

Abstract

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 practical complexity. We make several contributions. We propose a complete theoretical framework to specify and check real time properties on the formal model of a system. First, our framework provides a set of real time specification patterns (that may be viewed as a timed extension of Dwyer's patterns). We provide a verification technique based on the use of observers that has been implemented in a tool for the Fiacre modelling language. Finally, we provide two methods to check the correctness of our verification approach; a "semantics"-theoretical-method as well as a "graphical"-practical- method.

Mots-Clés / Keywords
Verification; Requirements; Specification patterns; Model checking; Observers; Real Time Systems;

128995
Les informations recueillies font l’objet d’un traitement informatique destiné à des statistiques d'utilisation du formulaire de recherche dans la base de données des publications scientifiques. Les destinataires des données sont : le service de documentation du LAAS.Conformément à la loi « informatique et libertés » du 6 janvier 1978 modifiée en 2004, vous bénéficiez d’un droit d’accès et de rectification aux informations qui vous concernent, que vous pouvez exercer en vous adressant à
Pour recevoir une copie des documents, contacter doc@laas.fr en mentionnant le n° de rapport LAAS et votre adresse postale. Signalez tout problème de dysfonctionnement à sysadmin@laas.fr. http://www.laas.fr/pulman/pulman-isens/web/app.php/