Retour au site du LAAS-CNRS

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

439documents trouvés

18137
28/06/2018

New model transformations for the stability analysis of time-delay systems

M.SAFI, L.BAUDOUIN, A.SEURET

ISI, MAC

Manifestation avec acte : IFAC Workshop on Time Delay Systems ( TDS ) 2018 du 28 juin au 30 juin 2018, Budapest (Hongrie), Juin 2018, 6p. , N° 18137

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

Diffusable

Plus d'informations

Abstract

This paper deals with the stability analysis of time delay systems based on continuous-time approach. The originality of the present paper relies on the construction of several models for a same time-delay systems using the interconnection of an ordinary differential equation and a transport partial differential equation. The stability analysis is then performed using a Lyapunov functional. These models are constructed in order to first reduce potentially the complexity of the resulting stability conditions. Second several models are build in order to be interpreted as a discretization scheme as the one usually used in the Lyapunov functional. The proposed result can be seen as a generalized (N − M) discretization which consists in both a time-discretization of the delay interval into M sub-intervals, and the projection of the state function within each sub-interval on the Legendre polynomials of degree less than N. The efficiency of this novel approach is illustrated on an academic example.

143735
18057
22/06/2018

Tomographic Node Placement Strategies and the Impact of the Routing Model

Y.A.PIGNOLET, S.SCHMID, G.TREDAN

ABB CRC, Switzerland, AAU, TSF

Manifestation avec acte : ACM Sigmetrics 2018 du 18 juin au 22 juin 2018, Irvine (USA), Juin 2018, 28p. , N° 18057

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

Diffusable

Plus d'informations

Abstract

Fault-tolerant computer networks rely on mechanisms supporting the fast detection of link failures. Tomo-graphic techniques can be used to implement such mechanisms at low cost: it is often sufficient to deploy a small number of tomography nodes exchanging probe messages along paths between them and detect link failures based on these messages. Our paper studies a practically relevant aspect of network tomography: the impact of the routing model. While the relevance of the routing model on path diversity and hence tomog-raphy cost is obvious and well-known on an anecdotal level, we lack an analytical framework to quantify the influence of different routing models (such as destination-based routing) exists. This paper fills this gap and introduces a formal model for asymmetric network tomography and a taxonomy of path routing models. This facilitates algorithmic reasoning about tomographic placement problems and quantifying the difference between routing models. In particular, we provide optimal and near-optimal algorithms to deploy a minimal number of asymmetric and symmetric tomography nodes for basic network topologies (modelled as graphs) under different routing model classes. Interestingly, we find that in many cases routing according to a more restrictive routing model gives better results: compared to a more general routing model, computing a good placement is algorithmically more tractable and does not entail high monitoring costs, a desirable trade-off in practice.

142813
18094
20/06/2018

SRide: A Privacy-Preserving Ridesharing System

U.M.AIVODJI, K.HUGUENIN, M.J.HUGUET, M.O.KILLIJIAN

TSF, HEC Lausanne, ROC

Manifestation avec acte : ACM Conference on Security and Privacy in Wireless and Mobile Networks ( WiSec ) 2018 du 18 juin au 20 juin 2018, Stockholm (Suède), Juin 2018 , N° 18094

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

Diffusable

143253
18140
12/06/2018

Lyapunov stability analysis of a system coupled to a hyperbolic PDE with potential

M.SAFI, A.SEURET, L.BAUDOUIN

ISI, MAC

Manifestation avec acte : European Control Conference ( ECC ) 2018 du 12 juin au 15 juin 2018, Limassol (Chypre), Juin 2018, 6p. , N° 18140

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

Diffusable

Plus d'informations

Abstract

This work deals with a stability problem for a system coupling an ordinary differential equation to a linear vectorial hyperbolic transport equation with a potential term. Using the Lyapunov methodology , a novel approach for stability of the coupled ODE-PDE system is developed. This methodology leads to a linear matrix inequality criteria while exploiting Bessel inequality and Legendre polynomials. To demonstrate the efficiency of this technique, the obtained criteria are applied on academic example.

143743
18136
11/06/2018

Adaptation dans les systèmes dynamiques : une vision informatique de la résilience

M.ROY

TSF

Habilitation à diriger des recherches : Juin 2018, 83p., Rapporteurs: P.FELBER, R.NAMYST, P.SENS, Examinateurs: L.DUCHIEN, A.FERNANDEZ ANTA, M.HERLIHY, P.QEUINNEC, Correspondant: J.C.FABRE , N° 18136

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

Diffusable

Plus d'informations

Abstract

Mes travaux comme chargé de recherche CNRS au LAAS-CNRS dans l’équipe Tolérance aux fautes et Sûreté de Fonctionnement informatique se sont articulés autour de l’adaptation dans les systèmes informatiques dynamiques, proposant une vision informatique du concept de résilience. Les contributions majeures développées lors de mes recherches s’organisent selon quatre axes : 1) l’architecture des systèmes leur permettant d’évoluer de manière sûre, à la fois pour la conception ex nihilo d’un système, que pour l’addition a posteriori de capacités adaptatives. 2) le déploiement de capacités d’observation et de vérification à l’exécution de propriétés pour permettre au système d’évaluer son état. 3) le développement d’algorithmes pour les systèmes répartis dynamiques prenant en compte la variation de la charge (concurrence) et la distribution dans l’espace physique. 4) la mesure et l’étude des systèmes informatiques (trans)portés par les humains. Les perspectives de ces travaux sont multiples et peuvent par exemple être organisées selon deux thèmes : 1) Comprendre les évolutions des systèmes dynamiques, dont le taux de pénétration dans la société, la taille et le niveau de criticité ne cesse d’augmenter. Il est nécessaire de capturer ces dynamiques nouvelles, en particulier issues de la dynamique humaine, pour fournir des jeux de données utilisables librement par les chercheurs, et proposer des modèles descriptifs et prédictifs de ces dynamiques. 2) Développer des mécanismes permettant de fournir des systèmes adaptables sûrs. L’avènement des multi-cœurs dans des domaines critiques (avionique, automobile) pose des défis immenses car ces puces augmentent la variabilité à l’exécution et donc la dynamique du système.

Mots-Clés / Keywords
Distributed computing; Dependability; Resilience; Adaptation; Mobile computing; Human Interactions;

143717
18113
02/06/2018

Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms

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

RIS, VERTICS, IDEA

Manifestation avec acte : International Conference on Formal Methods in Software Engineering ( FormaliSE ) 2018 du 02 juin au 02 juin 2018, Gothenburg (Suède), Juin 2018, 8p. , N° 18113

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

Diffusable

Plus d'informations

Abstract

Software constitutes a major part of the development of robotic and autonomous systems and is critical to their successful deployment in our everyday life. Robotic software must thus run and perform as specified. Since most of these systems are used in a hard real-time context, the schedulability of their tasks is a crucial property. In this work, we propose to use formal methods to check whether the tasks of a robotic application are schedulable with respect to a given hardware platform. For this, we automatically translate functional components specified in GenoM into FIACRE, a formal language for timed systems. The generated models integrate realistic real-time schedulers based on the FCFS and the SJF cooperative policies. We use then the model-checker TINA to assert schedulability properties. We carry out experiments on a real robotic system, namely a quadcopter flight controller. We demonstrate that, on its actual hardware, schedulability properties can be formally expressed and verified. We give examples on how we can check other important behavioral and timed properties on the same synthesized models.

143433
18126
22/05/2018

Time-accurate Middleware for the Virtualization of Communication Protocols

R.SCARDUELLI, P.A.BOURDIL, S.DAL ZILIO, D.LE BOTLAN

VERTICS, SCALIAN

Rapport LAAS N°18126, Mai 2018, 48p.

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

Diffusable

Plus d'informations

Abstract

Communication between devices in avionics systems must be predictable and deterministic, and data must be delivered reliably. To help the system architects comply with these requirements, network protocol standards like ARINC 429 and AFDX were created. Even though the behaviour of each component in a network is well defined, it is still necessary to test extensively every applications before deployment. But physical test benches used in the aircraft development process are complex and expensive platforms. In order to limit the need for physical tests, we propose a time-accurate middleware for virtualizing communication protocols that can be used to replace physical tests with simulations. We specified three formal models of AFDX networks that take into ac- count temporal constraints with different levels of precision. We also de- veloped a prototype for a network virtualization middleware based on the AFDX protocol specification that provides an easy-to-setup environment for testing network configurations. Finally, we used formal models together with virtualization in order to define runtime monitors for checking whether the behavior of the middleware is time-accurate with respect to a real system.

143553
18111
03/05/2018

Time-Efficient Read/Write Register in Crash-prone Asynchronous Message-Passing Systems

A.MOSTEFAOUI, M.RAYNAL, M.ROY

LS2N, IRISA, TSF

Revue Scientifique : Computing, 16p., Mai 2018 , N° 18111

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

Diffusable

Plus d'informations

Abstract

The atomic register is one of the most basic and useful object of computing science, and its simple read-write semantics is appealing when programming distributed systems. Hence, its implementation on top of crash-prone asynchronous message-passing systems has received a lot of attention. It was shown that having a strict minority of processes that may crash is a necessary and sufficient requirement to build an atomic register on top of a crash-prone asynchronous message-passing system. This paper visits the notion of a fast implementation of an atomic register, and presents a new time-efficient asynchronous algorithm that reduces latency in many cases: a write operation always costs a round-trip delay, while a read operation costs a round-trip delay in favorable circumstances (intuitively, when it is not concurrent with a write). When designing this algorithm, the design spirit was to be as close as possible to the original algorithm proposed by Attiya, Bar-Noy, and Dolev.

143413
18058
01/05/2018

Anomaly detection and diagnosis for cloud services: Practical experiments and lessons learned

C.SAUVANAUD, M.KAANICHE, K.KANOUN, K.LAZRI, G.DA SILVA SILVESTRE

TSF, Orange Labs, , ENAC

Revue Scientifique : Journal of Systems and Software, Vol.139, pp.84-106, Mai 2018 , N° 18058

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

Diffusable

Plus d'informations

Abstract

The dependability of cloud computing services is a major concern of cloud providers. In particular, anomaly detection techniques are crucial to detect anomalous service behaviors that may lead to the violation of service level agreements (SLAs) drawn with users. This paper describes an anomaly detec- tion system (ADS) designed to detect errors related to the erroneous behavior of the service, and SLA violations in cloud services. One major objective is to help providers to diagnose the anomalous virtual machines (VMs) on which a service is deployed as well as the type of error associated to the anomaly. Our ADS includes a system monitoring entity that collects software counters characterizing the cloud service, as well as a detection entity based on machine learning models. Additionally, a fault injection entity is integrated into the ADS for the training the machine learning models. This entity is also used to validate the ADS and to assess its anomaly detection and diagnosis performance. We validated our ADS with two case studies deployments: a NoSQL database, and a virtual IP Multimedia Subsystem developed implementing a virtual network function. Experimental results show that our ADS can achieve a high detection and diagnosis performance

142817
17013
01/05/2018

SMOF - A Safety MOnitoring Framework for Autonomous Systems

M.MACHIN, J.GUIOCHET, H.WAESELYNCK, J.P.BLANQUART, M.ROY, L.MASSON

TSF, ASTRIUM

Revue Scientifique : IEEE Transactions on Systems, Man, and Cybernetics: Systems, Vol.48, N°5, pp.702-715, Mai 2018, doi 10.1109/TSMC.2016.2633291 , N° 17013

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

Diffusable

Plus d'informations

Abstract

Safety critical systems with decisional abilities, such as autonomous robots, are about to enter our everyday life. Nevertheless, confidence in their behavior is still limited, particularly regarding safety. Considering the variety of hazards that can affect these systems, many techniques might be used to increase their safety. Among them, active safety monitors are a means to maintain the system safety in spite of faults or adverse situations. The specification of the safety rules implemented in such devices is of crucial importance, but has been hardly explored so far. In this paper, we propose a complete framework for the generation of these safety rules based on the concept of safety margin. The approach starts from a hazard analysis, and uses formal verification techniques to automatically synthesize the safety rules. It has been successfully applied to an industrial use case, a mobile manipulator robot for co-working.

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