Retour au site du LAAS-CNRS

Laboratoire d’analyse et d’architecture des systèmes

Publications de l'équipe VERTICS

Choisir la langue : FR | EN

55documents trouvés

16432
12/12/2016

De l'illustration du guidage à l'optimisation d'un plan par un robot Lego Mindstorm NXT

E.CHANTHERY, G.LE CORRE, P.E.HLADIK

DISCO, INSAT, VERTICS

Revue Scientifique : Journal sur l'enseignement des sciences et technologies de l'information et des, Vol.15, 12p., Décembre 2016 , N° 16432

Lien : https://hal.archives-ouvertes.fr/hal-01392601

Diffusable

Plus d'informations

Résumé

Cet article présente un projet mené au Département Génie Électrique et Informatique de l’Institut National des Sciences Appliquées (INSA) de Toulouse dont le but est la commande d’un robot Lego NXT. L’objectif est d’illustrer les différents niveaux de commande, du guidage bas niveau effectué par une régulation de position jusqu’à l’optimisation d’un plan de mission.

138343
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
16202
11/11/2016

Model checking real-time properties on the functional layer of autonomous robots

M.FOUGHALI, B.BERTHOMIEU, S.DAL ZILIO, F.INGRAND, A.MALLET

RIS, VERTICS, IDEA

Manifestation avec acte : International Conference on Formal Engineering Methods ( ICFEM ) 2016 du 11 novembre au 14 novembre 2016, Tokyo (Japon), Novembre 2016, 16p. , N° 16202

Lien : https://hal.archives-ouvertes.fr/hal-01346080

Diffusable

Plus d'informations

Abstract

Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example.

138502
16304
20/09/2016

Building confidence on formal verification models

P.A.BOURDIL, E.JENN, S.DAL ZILIO

VERTICS, IRT

Manifestation avec acte : Safecomp FastAbstract 2016 du 20 septembre au 23 septembre 2016, Trondheim (Norvège), Septembre 2016, 2p. , N° 16304

Lien : https://hal.laas.fr/hal-01369144

Diffusable

Plus d'informations

Abstract

A problem hindering the adoption of formal methods in the industry is how to integrate the models and results used during formal verification with existing processes. Indeed, formal verification is a complex process involving multiple methods, models, level of formality, ... If we want to use formal verification results in an assurance case, it is therefore necessary to build confidence on this process. The integration of formal methods raises particular problems like, for instance, with the construction of the verification models: a model may not preserve all properties of the system to be verified; it may only cover a subset of these properties; or it may be intractable. In practice, this means that the verification process involves a collection of models whose soundness (with the original system design, but also between each others) shall be justified. Furthermore, formal techniques are usually restricted in terms of the set of properties that can be checked. It is therefore necessary to justify (and trace back) that these restrictions are consistent with the hypotheses made about the system, its application and its environment. This short abstract gives an overview of a methodology for building verification arguments, that is convincing arguments that a system design complies with a set of properties.

137595
16115
07/07/2016

Integrating model checking in an industrial verification process: a structuring approach

P.A.BOURDIL, S.DAL ZILIO, E.JENN

VERTICS, IRT

Rapport LAAS N°16115, Juillet 2016, 13p.

Lien : https://hal.archives-ouvertes.fr/hal-01341701

Diffusable

Plus d'informations

Abstract

An obstacle to the adoption of model-checking in large projects is a lack of guidelines on how to integrate formal methods with existing system engineering practices. In this context, a methodology should give answers to several questions: How to manage the models and abstractions used to verify a claim? How do we gain confidence on the soundness of these models? How can we build a structured argument from the verification results? In this paper , we describe a structured approach for managing verification arguments an apply it to check a critical function of an autonomous rover.

136852
16182
07/06/2016

Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées

P.E.HLADIK, S.DAL ZILIO, O.PASQUIER, S.PILLEMENT, B.BERTHOMIEU

VERTICS, IETR-CNRS

Manifestation avec acte : Approches Formelles dans l'Assistance au Développement de Logiciels ( AFADL ) 2016 du 07 juin au 08 juin 2016, Besançon (France), Juin 2016, 7p. , N° 16182

Lien : https://hal.archives-ouvertes.fr/hal-01331726

Diffusable

Plus d'informations

Résumé

Cet article présente un travail en cours pour mettre en place une chaîne d'outils dédiée à la conception, la vérification et l'exécution de systèmes embarqués temps réel. Ce travail se base sur la méthode MCSE et les modèles qu'elle préconise pour la description d'applications. Une traduction du modèle dans le langage formel Fiacre est appliquée pour ensuite vérifier le système à l'aide du model-checker Tina. Afin de faciliter cette analyse et la génération d'un exécutif, la notion de Logical Execution Time est utilisée pour décrire le comportement tem-porel. Nous présentons ces différentes méthodes et outils avant d'exposer l'état d'avancement des différents composants de la chaîne.

137075
16049
15/03/2016

Fast and tight analysis for AUTOSAR schedule tables

P.E.HLADIK

VERTICS

Rapport LAAS N°16049, Mars 2016, 26p.

Lien : https://hal.archives-ouvertes.fr/hal-01273673

Diffusable

Plus d'informations

Abstract

AUTOSAR is the name of a consortium that defines a set of industrial standards for the design of in-vehicle embedded systems. The AUTOSAR consortium promotes a model-based approach, supported by tools that are expected to automatically transform a functional design into a real-time multitask software. Before to consider the design of such tools, one must be able to verify the real-time behavior of a multitask software. This report presents an extension of a previous work on a mathematical modeling framework for AUTOSAR applications and a worst-case response time analysis [7, 8, 9] published with Anne-Marie Déplanche, Sébastien Faucou and Yvon Trinquet. Three new algorithms are proposed, implemented and evaluated to improve performance of the analysis

136336
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
15357
05/10/2015

On the complexity of flanked finite state automata

F.AVELLANEDA, S.DAL ZILIO, J.B.RACLET

IRIT, VERTICS

Rapport LAAS N°15357, Octobre 2015, 16p.

Lien : https://hal.archives-ouvertes.fr/hal-01202702

Diffusable

Plus d'informations

Abstract

We define a new subclass of nondeterministic finite automata for prefix-closed languages called Flanked Finite Automata (FFA). We show that this class enjoys good complexity properties while preserving the succinctness of nondeterministic automata. In particular, we show that the universality problem for FFA is in linear time and that language inclusion can be checked in polynomial time. A useful application of FFA is to provide an efficient way to compute the quotient and inclusion of regular languages without the need to use the powerset construction. These operations are the building blocks of several verification algorithms.

135346
15355
05/10/2015

Latency analysis of an aerial video tracking system using fiacre and tina

S.DAL ZILIO, B.BERTHOMIEU, D.LE BOTLAN

VERTICS

Rapport LAAS N°15355, Octobre 2015

Lien : https://hal.archives-ouvertes.fr/hal-01202741

Diffusable

Plus d'informations

Abstract

We describe our experience with modeling a video tracking system used to detect and follow moving targets from an airplane. We provide a formal model that takes into account the real-time properties of the system and use it to compute the worst and best-case end to end latency. We also compute a lower bound on the delay between the loss of two frames. Our approach is based on the model-checking tool Tina, that provides state-space generation and model-checking algorithms for an extension of Time Petri Nets with data and priorities. We propose several models divided in two main categories: first Time Petri Net models, which are used to study the behavior of the system in the most basic way; then models based on the Fiacre specification language, where we take benefit of richer data structures to directly model the buffering of video information and the use of an unbounded number of frame identifiers.

135343
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/